一句话：提出结构化时序逻辑 ticl，将复杂（余）归纳证明编码为结构引理，在证明助手中以高抽象层次对无限程序的安全性/活性进行组合式验证。
对带效应与非确定性的无限程序进行机器化活性验证十分困难。现有工作多在迹、自动机等模型层面推理，需使用复杂的嵌套（余）归纳技术并熟悉证明助手的守卫性检查，且脱离程序构造，丧失了 Hoare 逻辑等结构程序逻辑的模块化与组合性。为此，作者提出结构化时序逻辑 ticl，把复杂的（余）归纳证明技术编码为结构引理，使验证者只需关注 variant 与 invariant。论文在证明助手中实现了组合式、高层次的一般时序性质证明，并对调度、并发共享内存和分布式共识程序给出安全性与活性的机器化证明，且证明与代码比很低。
Mechanized verification of liveness properties for infinite programs with effects and nondeterminism is challenging. Existing temporal reasoning frameworks operate at the level of models such as traces and automata. Reasoning happens at a very low-level, requiring complex nested (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., the guardedness checker). Further, reasoning at the level of models instead of program constructs creates a verification gap that loses the benefits of modularity and composition enjoyed by structural program logics such as Hoare Logic. To address this verification gap, and the lack of compositional proof techniques for temporal specifications, we propose ticl , a new structural temporal logic. Using ticl , we encode complex (co-)inductive proof techniques as structural lemmas and focus our reasoning on variants and invariants. We show that it is possible to perform compositional proofs of general temporal properties in a proof assistant, while working at a high level of abstraction. We demonstrate the benefits of ticl by giving mechanized proofs of safety and liveness properties for programs with scheduling, concurrent shared memory, and distributed consensus, demonstrating a low proof-to-code ratio.
@article{paperbot2965,
title = {Structural Temporal Logic for Mechanized Program Verification},
author = {Eleftherios Ioannidis and Yannick Zakowski and Steve Zdancewic and Sebastian Angel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763091}
}