Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. Property-Directed Inference of Universal Invariants or Proving Their Absence. Journal of ACM, 64(1):7:1--7:33, 2017.
We present Universal Property Directed Reachability (UPDR), a property-directed semi-algorithm for automatic inference of invariants in a universal fragment of first-order logic. UPDR is an extension of Bradley's PDR/IC3 algorithm for inference of propositional invariants. UPDR terminates when it either 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. UPDR is not guaranteed to terminate. However, we prove that under certain conditions, e.g., when reasoning about programs manipulating singly-linked lists, it does. We implemented an analyzer based on UPDR, 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.