Title: Counterexample-Guided k-Induction Verification for Fast Bug Detection,
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.