Další formáty:
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 a 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, s.~268-282. ISBN~978-3-319-22968-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-22969-0\_{}19.
|