Boosting k‑Induction with Continuously‑Refined Invariants

Dirk Beyer


Matthias Dangl



Philipp Wendler


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-flow-based 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 continuously-refined invariants significantly increases effectiveness and efficiency, and outperforms all existing implementations of k‑induction-based verification of C programs in terms of successful results.

A preprint of our published article is available for you to download.


We provide a virtual machine with an installation of the tools that can be used to easily reproduce our experimental results. The username is cav, the password is ae. This virtual machine has been approved by the CAV Artifact Evaluation Committee.

The supplementary archive contains all data from our experiments. The following files are in this archive:


The result tables of the figures in our article are also available:

You can click on the cells in the status columns of the CPAchecker configurations in these tables to see their output. Due to their size, the log files of CBMC and ESBMC are not included in the online version, but the data, including the tables with clickable cells, are available in the downloadable supplementary archive.