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 also reduced considerably.
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 also reduced considerably.
| Original language | English |
|---|---|
| Title of host publication | 25th ACM SIGSOFT International Symposium on the Foundations of Software Engineering |
| DOIs | |
| Publication status | Published - 2018 |
Keywords
- Bounded model checking
- k-induction
- Formal Software Verification
- Bug detection