Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space

TL;DR

This paper introduces bidirectional k-induction (bkind), a novel proof rule that leverages counterexamples to improve bug detection and verification efficiency in model checking, outperforming existing methods.

Contribution

The paper presents bkind, a new k-induction technique that uses counterexamples to enhance bug detection and verification, combined with an interval invariant generator for better results.

Findings

bkind reduces verification time by half compared to naive k-induction

bkind outperforms 2LS in correctness and proof generation

bkind achieves 35% more correct alarms on benchmark sets

Abstract

We describe and evaluate a novel k-induction proof rule called bidirectional k-induction (bkind), which substantially improves the k-induction bug-finding capabilities. Particularly, bkind exploits the counterexamples generated by the over-approximation step to derive new properties and feed them back to the bounded model checking procedure. We also combine an interval invariant generator and bkind to significantly improve the number of correct verification results. Experimental results show that bkind can considerably reduce the verification time compared to the naive k-induction proof rule, since it only requires half the number of steps to find a given safety property violation in an unsafe program. The bkind algorithm outperforms 2LS, another state-of-the-art k-induction verifier, and produces more than twice correct proofs and about 35% more correct alarms than when analysing a large set of public available benchmarks.