Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1352234,
author = {Štill, Vladimír and Ročkai, Petr and Barnat, Jiří},
address = {New York, NY, USA},
booktitle = {Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
doi = {http://dx.doi.org/10.1007/978-3-662-49674-9_60},
editor = {M. Chechik and J.-F. Raskin},
keywords = {DIVINE model checker; LTL model checking},
howpublished = {tištěná verze "print"},
language = {eng},
location = {New York, NY, USA},
isbn = {978-3-662-49673-2},
pages = {920-922},
publisher = {Springer-Verlag New York, Inc.},
title = {DIVINE: Explicit-State LTL Model Checker},
url = {http://dx.doi.org/10.1007/978-3-662-49674-9_60},
year = {2016}
}
TY - JOUR
ID - 1352234
AU - Štill, Vladimír - Ročkai, Petr - Barnat, Jiří
PY - 2016
TI - DIVINE: Explicit-State LTL Model Checker
PB - Springer-Verlag New York, Inc.
CY - New York, NY, USA
SN - 9783662496732
KW - DIVINE model checker
KW - LTL model checking
UR - http://dx.doi.org/10.1007/978-3-662-49674-9_60
N2 - DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.
ER -
ŠTILL, Vladimír, Petr ROČKAI and Jiří BARNAT. DIVINE: Explicit-State LTL Model Checker. In M. Chechik and J.-F. Raskin. \textit{Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems}. New York, NY, USA: Springer-Verlag New York, Inc., 2016, p.~920-922. ISBN~978-3-662-49673-2. Available from: https://dx.doi.org/10.1007/978-3-662-49674-9\_{}60.
|
