用于机械化程序验证的结构时序逻辑

《Proceedings of the ACM on Programming Languages》：Structural Temporal Logic for Mechanized Program Verification

机械验证无限有效应非确定性程序生命性质的困难，现有框架在模型层面低级推理依赖复杂归纳证明，导致模块性和组合优势丧失。Ticl结构化时间逻辑将归纳证明转化为结构引理，实现高抽象层次可组合证明，成功验证调度系统、并发共享内存和分布式共识场景，证明代码效率显著提升。

　　

摘要

对于具有副作用和非确定性的无限程序，实现其活性属性的自动化验证具有挑战性。现有的时序推理框架主要在模型层面（如轨迹和自动机）进行操作。这些推理过程处于非常底层的层次，需要复杂的嵌套（协同）归纳证明技术以及对证明辅助工具（例如保护性检查器）的熟悉程度。此外，仅在模型层面进行推理而忽略程序结构本身，会导致验证过程中无法充分利用结构化程序逻辑（如Hoare逻辑）所具备的模块化和组合性优势。为了解决这一验证难题以及时序规范缺乏组合性证明技术的问题，我们提出了一种新的结构化时序逻辑——Ticl。通过使用Ticl，我们将复杂的（协同）归纳证明技术编码为结构化引理，并将推理重点放在程序的变体和不变量上。我们证明了在高级抽象层次上，仍然可以在证明辅助工具中完成对一般时序属性的组合性证明。通过为具有调度、并发共享内存和分布式共识特性的程序提供自动化证明，我们展示了Ticl的优势，同时实现了较低的证明代码比（即证明过程所需代码量的比例）。