Property-directed inference of universal invariants or proving their absence

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

DOI

  • Aleksandr Karbyshev
  • ,
  • Nikolaj Bjørner, Microsoft Research
  • ,
  • Shachar Itzhaky, Massachusetts Institute of Technology
  • ,
  • Noam Rinetzky, Tel Aviv University
  • ,
  • Sharon Shoham, Tel Aviv University

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.

Original languageEnglish
Article number7
JournalJournal of the ACM
Volume64
Issue1
Pages (from-to)7:1-7:33
Number of pages33
ISSN0004-5411
DOIs
Publication statusPublished - 29 Mar 2017

    Research areas

  • EPR, IC3, PDR, Property-directed reachability, Universal invariants

See relations at Aarhus University Citationformats

ID: 118502925