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-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.
Content
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 additional test-set definitions and configurations required for the paper
- The CBMC executable (version 5.1) and k‑Induction wrapper script provided by Michael Tautschnig
- ESBMC version 2.25.2 and a wrapper script for k‑Induction with ESBMC based on the ESBMC submission to SV-COMP 2013 as recommended by Lucas Cordeiro
- The results presented in our paper
- A README file explaining how to reproduce the results
Results
The result tables of the figures in our article are also available:
- k‑Induction comparison between CBMC, ESBMC (sequential and parallel versions) and CPAchecker
- Comparison between the CPAchecker implementations of k‑Induction
- A comparison between the CPAchecker implementations of predicate analysis, value analysis, and k‑Induction using continuously-refined invariant generation
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.