Inductive invariant generation via abductive inference
Citations Over TimeTop 1% of 2013 papers
Abstract
This paper presents a new method for generating inductive loop invariants that are expressible as boolean combinations of linear integer constraints. The key idea underlying our technique is to perform a backtracking search that combines Hoare-style verification condition generation with a logical abduction procedure based on quantifier elimination to speculate candidate invariants. Starting with true, our method iteratively strengthens loop invariants until they are inductive and strong enough to verify the program. A key feature of our technique is that it is lazy: It only infers those invariants that are necessary for verifying program correctness. Furthermore, our technique can infer arbitrary boolean combinations (including disjunctions) of linear invariants. We have implemented the proposed approach in a tool called HOLA. Our experiments demonstrate that HOLA can infer interesting invariants that are beyond the reach of existing state-of-the-art invariant generation tools.
Related Papers
- → A Fault-Localization Approach Based on the Coincidental Correctness Probability(2015)6 cited
- → Local quantifier elimination(2000)6 cited
- A constraint satisfaction approach to the resolution of uncertainty in image interpretation(1992)
- Distributed Valued Constraint Networks and Backtracking(2008)
- → Correctness and Bounded Correctness [Keynote Address](2019)