salle A. Turing CE4
6 juin 2014 - 14h00
Combining k-Induction with Continuously-Refined Invariants
par Philipp Wendler de Universität Passau
Abstract: Bounded model checking (BMC) is a well-known and successful technique for finding bugs in software.
k-induction is an approach to extend BMC-based approaches from falsification to verification.
Automatically generated auxiliary invariants can be used to strengthen
the induction hypothesis. We improve this approach and further increase effectiveness and
efficiency in the following way: we start with light-weight invariants
and refine these invariants continuously during the analysis.
Our experiments show that combining k-induction with continuously-refined invariants increases effectiveness and efficiency in comparison with the state of the art in k-induction-based software verification.
In a second part of the talk, we see how such an analysis can be integrated
into the open-source software verification framework CPAchecker by leveraging techniques such as configurable software verification and reusing existing analyses.
