Context-Switch-Directed Verification in DIVINE

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ŠTILL Vladimír ROČKAI Petr BARNAT Jiří

Year of publication 2014
Type Article in Proceedings
Conference Mathematical and Engineering Methods in Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-14896-0_12
Field Informatics
Keywords model checking; LLVM; context-switch bounded verification
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.