Property-Directed Inference of Universal Invariants or Proving Their Absence
Property-Directed Inference of Universal Invariants or Proving Their Absence
复制标题
通用不变量的属性导向推理或证明它们的不存在
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Sharon Shoham
中科院分区：
文献类型：
--
作者：
Aleksandr Karbyshev;Nikolaj S. Bjørner;Shachar Itzhaky;N. Rinetzky;Sharon Shoham
我们提出了通用属性定向可达性（PDR），一个属性定向的半自动推理的一阶逻辑的通用片段的不变量的算法。PDR是布拉德利用于命题不变量推理的PDR/IC 3算法的扩展。当PDR发现一个具体的反例，推断出一个足够强的归纳通用不变量来建立所需的安全属性，或者找到一个证明这样的不变量不存在的证据时，PDR终止。PDR不保证终止。然而，我们证明，在某些条件下，例如，当推理程序操纵单链表，它。我们实现了一个分析器的基础上的PDR？并将其应用到列表操作程序的集合。我们的分析器能够自动推断出足够强大的通用不变量，以建立内存安全性和某些功能正确性属性，显示某些自然程序和规范的不变量，并检测错误。所有这一切都不需要用户提供的抽象谓词。
We present Universal Property Directed Reachability (PDR∀), a property-directed semi-algorithm for automatic inference of invariants in a universal fragment of first-order logic. PDR∀ is an extension of Bradley’s PDR/IC3 algorithm for inference of propositional invariants. PDR∀ terminates when it discovers a concrete counterexample, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a proof that such an invariant does not exist. PDR∀ is not guaranteed to terminate. However, we prove that under certain conditions, for example, when reasoning about programs manipulating singly linked lists, it does. We implemented an analyzer based on PDR∀ and applied it to a collection of list-manipulating programs. Our analyzer was able to automatically infer universal invariants strong enough to establish memory safety and certain functional correctness properties, show the absence of such invariants for certain natural programs and specifications, and detect bugs. All this without the need for user-supplied abstraction predicates.
空间插值
DOI：
10.48550/arxiv.1501.04100
发表时间：
2015
期刊：
arXiv e-prints
影响因子：
--
作者：
Albarghouthi Aws
通讯作者：
Albarghouthi Aws
反例引导焦点
DOI：
10.1145/1706299.1706330
发表时间：
2010
期刊：
影响因子：
--
作者：
A. Podelski;T. Wies
通讯作者：
T. Wies