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的优势。