Context-Switch-Directed Verification in DIVINE

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	ŠTILL Vladimír ROČKAI Petr BARNAT Jiří
Rok publikování	2014
Druh	Článek ve sborníku
Konference	Mathematical and Engineering Methods in Computer Science
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Doi	http://dx.doi.org/10.1007/978-3-319-14896-0_12
Obor	Informatika
Klíčová slova	model checking; LLVM; context-switch bounded verification
Popis	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.
Související projekty:	Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.