Beautiful interpolants

A Albarghouthi, KL McMillan - … , CAV 2013, Saint Petersburg, Russia, July …, 2013 - Springer
Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013Springer
We describe a compositional approach to Craig interpolation based on the heuristic that
simpler proofs of special cases are more likely to generalize. The method produces simple
interpolants because it is able to summarize a large set of cases using one relatively simple
fact. In particular, we present a method for finding such simple facts in the theory of linear
rational arithmetic. This makes it possible to use interpolation to discover inductive invariants
for numerical programs that are challenging for existing techniques. We show that in some …
Abstract
We describe a compositional approach to Craig interpolation based on the heuristic that simpler proofs of special cases are more likely to generalize. The method produces simple interpolants because it is able to summarize a large set of cases using one relatively simple fact. In particular, we present a method for finding such simple facts in the theory of linear rational arithmetic. This makes it possible to use interpolation to discover inductive invariants for numerical programs that are challenging for existing techniques. We show that in some cases, the compositional approach can also be more efficient than traditional lazy SMT as a decision procedure.
Springer