论文标题
诱导环推理的痕量逻辑
Trace Logic for Inductive Loop Reasoning
论文作者
论文摘要
我们提出了Trace Logic，这是多组一阶逻辑的实例，以自动化包含循环程序的部分正确性验证。 Trace Logic通过在任意时间点和循环迭代中编码属性来概括程序位置的语义并捕获循环语义。我们使用通用的痕量引理捕获电感回路不变性，并在微量逻辑中引导和自动化诱导环路推理。我们的工作是在快速范围内扩展和集成基于叠加的一阶推理的快速框架中实施的。我们成功使用快速证明了许多程序的正确性，这些程序的功能行为最好总结在线性整数算术，阵列和归纳数据类型的一阶理论中。
We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturing inductive loop invariants. Our work is implemented in the RAPID framework, by extending and integrating superposition-based first-order reasoning within RAPID. We successfully used RAPID to prove correctness of many programs whose functional behavior are best summarized in the first-order theories of linear integer arithmetic, arrays and inductive data types.
