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.
|