Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1316721,
author = {Ročkai, Petr and Štill, Vladimír and Barnat, Jiří},
address = {Neuveden},
booktitle = {Software Engineering and Formal Methods},
doi = {http://dx.doi.org/10.1007/978-3-319-22969-0_19},
editor = {Radu Calinescu, Bernhard Rumpe},
keywords = {LLVM; model checking; compression; memory-efficient; explicit-state},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Neuveden},
isbn = {978-3-319-22968-3},
pages = {268-282},
publisher = {Springer International Publishing},
title = {Techniques for Memory-Efficient Model Checking of C and C++ Code},
year = {2015}
}
TY - JOUR
ID - 1316721
AU - Ročkai, Petr - Štill, Vladimír - Barnat, Jiří
PY - 2015
TI - Techniques for Memory-Efficient Model Checking of C and C++ Code
PB - Springer International Publishing
CY - Neuveden
SN - 9783319229683
KW - LLVM
KW - model checking
KW - compression
KW - memory-efficient
KW - explicit-state
N2 - We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs. As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untime-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storage in a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty.
ER -
ROČKAI, Petr, Vladimír ŠTILL and Jiří BARNAT. Techniques for Memory-Efficient Model Checking of C and C++ Code. In Radu Calinescu, Bernhard Rumpe. \textit{Software Engineering and Formal Methods}. Neuveden: Springer International Publishing, 2015, p.~268-282. ISBN~978-3-319-22968-3. Available from: https://dx.doi.org/10.1007/978-3-319-22969-0\_{}19.
|
