| ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Context-Switch-Directed Verification in DIVINE. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. Mathematical and Engineering Methods in Computer Science. Neuveden: Springer International Publishing, 2014, s. 135-146. ISBN 978-3-319-14895-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-14896-0_12. |
Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1316718,
author = {Štill, Vladimír and Ročkai, Petr and Barnat, Jiří},
address = {Neuveden},
booktitle = {Mathematical and Engineering Methods in Computer Science},
doi = {http://dx.doi.org/10.1007/978-3-319-14896-0_12},
editor = {Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala},
keywords = {model checking; LLVM; context-switch bounded verification},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Neuveden},
isbn = {978-3-319-14895-3},
pages = {135-146},
publisher = {Springer International Publishing},
title = {Context-Switch-Directed Verification in DIVINE},
year = {2014}
}
TY - JOUR
ID - 1316718
AU - Štill, Vladimír - Ročkai, Petr - Barnat, Jiří
PY - 2014
TI - Context-Switch-Directed Verification in DIVINE
PB - Springer International Publishing
CY - Neuveden
SN - 9783319148953
KW - model checking
KW - LLVM
KW - context-switch bounded verification
N2 - 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.
ER -
ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Context-Switch-Directed Verification in DIVINE. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. \textit{Mathematical and Engineering Methods in Computer Science}. Neuveden: Springer International Publishing, 2014, s.~135-146. ISBN~978-3-319-14895-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-14896-0\_{}12.
|
