Loop invariants from counterexamples

Abstract

We propose a new approach to software model checking where we integrate abstract interpretation and trace abstraction. We use abstract interpretation to derive loop invariants for the path program corresponding to a given spurious counterexample. A path program is the smallest subprogram that still contains a given path in the control flow graph. We use the principle of trace abstraction to construct an overall proof. The key observation of our approach is that proofs by abstract interpretation on individual program fragments can be composed directly if we use the framework of trace abstraction (in trace abstraction, composing proofs amounts to a set-theoretic operation, i.e., set union). We implemented our approach in the open-source software model checking framework Ultimate. Our evaluation shows that we can solve up to 40% more benchmarks.