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 ex- ploration 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
Published in: Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146.