Trabalho em anais de eventoOpen Access
Towards Counterexample-guided k-Induction for Fast Bug Detection
GADELHA, M. Y. R.; SOUSA, F. R. M.; CORDEIRO, L. C.; NICOLE, D
Resumo
Resumo
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 extend the k-induction algorithm 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 main advantage is in the reduction of the state explosion by reducing the maximum required steps from k to ⌊k/2 + 1⌋.
palavras-chave
Palavras-chave
k-inductioncounterexample-guided inductive synthesisbug detectionbidirectional searchstate space explosionover-approximationprogram verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento