Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1082157,
author = {Barnat, Jiří and Havlíček, Jan and Ročkai, Petr},
address = {Neuveden},
booktitle = {Electronic Notes in Theoretical Computer Science, Volume 296},
doi = {http://dx.doi.org/10.1016/j.entcs.2013.07.006},
keywords = {model checking; LTL; hash compaction},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Neuveden},
pages = {79-93},
publisher = {Elsevier Science},
title = {Distributed LTL Model Checking with Hash Compaction},
url = {http://dx.doi.org/10.1016/j.entcs.2013.07.006},
year = {2013}
}
TY - JOUR
ID - 1082157
AU - Barnat, Jiří - Havlíček, Jan - Ročkai, Petr
PY - 2013
TI - Distributed LTL Model Checking with Hash Compaction
PB - Elsevier Science
CY - Neuveden
KW - model checking
KW - LTL
KW - hash compaction
UR - http://dx.doi.org/10.1016/j.entcs.2013.07.006
L2 - http://dx.doi.org/10.1016/j.entcs.2013.07.006
N2 - We extend a distributed-memory explicit-state LTL model checking algorithm (OWCTY) with hash compaction. We provide a detailed description of the improved algorithm and a correctness argument in the theoretical part of the paper. Additionally, we deliver an implementation of the algorithm as part of out parallel and distributed-memory model checker DiVinE, and use this implementation for a practical evaluation of the approach, on which we report in the experimental part of the paper.
ER -
BARNAT, Jiří, Jan HAVLÍČEK and Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In \textit{Electronic Notes in Theoretical Computer Science, Volume 296}. Neuveden: Elsevier Science, 2013, p.~79-93. ISSN~1571-0661. Available from: https://dx.doi.org/10.1016/j.entcs.2013.07.006.
|
