Context-Switch-Directed Verification in DIVINE

March 3, 2020

In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.

Authors: Vladimír Štill, Petr Ročkai, Jiří Barnat

Project: DIVINE4

Published in: Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146.

Go to pdf

Article Link

Authors

Partner University

Collaborations

Institutes

Associated Research Projects