Counterexample-Guided k-Induction Verification for Fast Bug Detection

TL;DR

This paper introduces a bidirectional k-induction algorithm that efficiently detects bugs by reducing verification steps and time, especially in large state space programs.

Contribution

It extends the k-induction method into a meet-in-the-middle search using counterexamples, improving bug detection efficiency.

Findings

Reduces steps to find property violations to approximately half of k.

Significantly decreases verification time for large state space programs.

Preliminary results demonstrate improved bug detection efficiency.

Abstract

Recently, the k-induction algorithm has proven to be a successful approach for both finding bugs and proving correctness. However, since the algorithm is an incremental approach, it might waste resources trying to prove incorrect programs. In this paper, we propose to extend the k-induction algorithm in order to shorten the number of steps required to find a property violation. We convert the algorithm into a meet-in-the-middle bidirectional search algorithm, using the counterexample produced from over-approximating the program. The preliminary results show that the number of steps required to find a property violation is reduced to $\lfloor\frac{k}{2} + 1\rfloor$ and the verification time for programs with large state space is reduced considerably.