Boosting k-induction with continuously-refined invariants

Abstract

k-induction is a promising technique to extend bounded model checking from falsification to verification. In software verification, k-induction works only if auxiliary invariants are used to strengthen the induction hypothesis. The problem that we address is to generate such invariants (1) automatically without user-interaction, (2) efficiently such that little verification time is spent on the invariant generation, and (3) that are sufficiently strong for a k-induction proof. We boost the k-induction approach to significantly increase effectiveness and efficiency in the following way: We start in parallel to k-induction a data-flowbased invariant generator that supports dynamic precision adjustment and refine the precision of the invariant generator continuously during the analysis, such that the invariants become increasingly stronger. The k-induction engine is extended such that the invariants from the invariant generator are injected in each iteration to strengthen the hypothesis. The new method solves the above-mentioned problem because it (1) automatically chooses an invariant by step-wise refinement, (2) starts always with a lightweight invariant generation that is computationally inexpensive, and (3) refines the invariant precision more and more to inject stronger and stronger invariants into the induction system. We present and evaluate an implementation of our approach, as well as all other existing approaches, in the open-source verification-framework CPAchecker. Our experiments show that combining k-induction with continuouslyrefined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k-induction-based verification of C programs in terms of successful results.