Boosting Automated Verification Using Cyclic Proof

使用循环证明增强自动验证

• 批准号: EP/K040049/1
• 负责人: James Brotherston
• 金额: $ 70.1万
• 依托单位: University College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2013
• 资助国家: 英国
• 起止时间: 2013 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FK040049%2F1
• 关键词: Boosting; Automated; Verification; Using; Cyclic

Automatic verification tools based on separation logic have recently enabled the verification of code bases that scale into the millions of lines. Such analyses rely on the use of *inductive predicates* to describe data structures held in memory. However, such predicates are currently hard-coded into the analysis, which means that the analysis must fail when encountering an unknown data structure, not described by the hard-coded definitions. This results in reduced program coverage and increased rates of false negatives. Thus, methods for reasoning with *general* inductively defined predicates could greatly enhance the state of the art.Cyclic proof, in essence, implements reasoning by infinite descent à la Fermat for general inductive definitions. In contrast to traditional proofs by explicit induction, which force the prover to select the induction schema and hypotheses at the very beginning of a proof, cyclic proof allows these difficult decisions to be *postponed* until exploration of the proof search space makes suitable choices more evident. This makes cyclic proof an attractive method for automatic proof search.The main contention of this proposal is that cyclic proof techniques can add inductive reasoning capability, for general inductive predicates, to the many components of an interprocedural program analysis (theorem proving, abduction, frame-inference, abstraction) and thus can significantly extend the reach of current verification methods.

基于分离逻辑的自动验证工具最近已经能够验证扩展到数百万行的代码库。这种分析依赖于使用 * 归纳谓词 * 来描述内存中保存的数据结构。然而，这些谓词目前被硬编码到分析中，这意味着当遇到未知的数据结构时，分析必须失败，而不是由硬编码的定义描述。这会导致程序覆盖率降低和假阴性率增加。因此，用 * 一般 * 归纳定义的谓词进行推理的方法可以大大提高现有技术的水平。循环证明，本质上，实现了对一般归纳定义的无限下降的推理。与传统的显式归纳证明相反，它迫使证明者在证明的最开始就选择归纳模式和假设，循环证明允许这些困难的决定被推迟，直到证明搜索空间的探索使得合适的选择更加明显。这使得循环证明一个有吸引力的方法，自动proof search.This建议的主要论点是，循环证明技术可以增加归纳推理能力，一般归纳谓词，许多组件的过程间程序分析（定理证明，溯因推理，框架推理，抽象），从而可以显着扩展目前的验证方法的范围。

项目成果

Automatic cyclic termination proofs for recursive procedures in separation logic

• DOI: 10.1145/3018610.3018623
• 发表时间: 2017-01
• 期刊: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
• 作者: R. Rowe;J. Brotherston

Static Analysis

静态分析

• DOI: 10.1007/978-3-642-38856-9_22
• 发表时间: 2013
• 作者: Brain M

Automated Reasoning with Analytic Tableaux and Related Methods

使用分析表和相关方法进行自动推理

• DOI: 10.1007/978-3-642-40537-2_17
• 发表时间: 2013
• 作者: Khodadadi M