# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1904.02501