Mechanized verification of liveness properties for programs with effects, nondeterminism, and nontermination is difficult. Existing temporal reasoning frameworks operate on the level of models (traces, automata) not executable code, creating a verification gap and losing the benefits of modularity and composition enjoyed by structural program logics. Reasoning about infinite traces and automata requires complex (co-)inductive proof techniques and familiarity with proof assistant mechanics (e.g., guardedness checker). We propose a structural approach to the verification of temporal properties with a new temporal logic that we call Ticl. Using Ticl, we internalize complex (co-)inductive proof techniques to structural lemmas and reasoning about variants and invariants. We show that it is possible to perform mechanized proofs of general temporal properties, while working in a high-level of abstraction. We demonstrate the benefits of ticl by giving short, structural proofs of safety and liveness properties for programs with queues, secure memory, and distributed consensus.

翻译：针对具有副作用、非确定性和非终止性的程序，其活性性质的机械化验证是困难的。现有的时序推理框架在模型层面（迹、自动机）而非可执行代码层面操作，这造成了验证鸿沟，并丧失了结构化程序逻辑所具备的模块化和组合性优势。对无限迹和自动机进行推理需要复杂的（共）归纳证明技术，并需熟悉证明辅助工具机制（例如，守卫性检查器）。我们提出了一种验证时序性质的结构化方法，该方法基于一种我们称之为Ticl的新时序逻辑。利用Ticl，我们将复杂的（共）归纳证明技术内化为结构化引理以及对变体和不变量的推理。我们证明，在高层抽象层面工作的同时，对一般时序性质进行机械化证明是可能的。我们通过为具有队列、安全内存和分布式共识的程序提供简短的结构化安全性与活性证明，展示了Ticl的优势。