Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1130020, author = {Ročkai, Petr and Barnat, Jiří and Brim, Luboš}, address = {Neuveden}, booktitle = {NASA Formal Methods 2013}, doi = {http://dx.doi.org/10.1007/978-3-642-38088-4_1}, editor = {Guillaume Brat, Neha Rungta, Arnaud Venet}, keywords = {model checking; C; C++; LTL; LLVM; DIVINE}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Neuveden}, isbn = {978-3-642-38087-7}, pages = {1-15}, publisher = {Springer}, title = {Improved State Space Reductions for LTL Model Checking of C & C++ Programs}, year = {2013} }
TY - JOUR ID - 1130020 AU - Ročkai, Petr - Barnat, Jiří - Brim, Luboš PY - 2013 TI - Improved State Space Reductions for LTL Model Checking of C & C++ Programs PB - Springer CY - Neuveden SN - 9783642380877 KW - model checking KW - C KW - C++ KW - LTL KW - LLVM KW - DIVINE N2 - In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C &; C++ programs, building on~\cite{BBR12b}, including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction. ER -
ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Improved State Space Reductions for LTL Model Checking of C \&{} C++ Programs. In Guillaume Brat, Neha Rungta, Arnaud Venet. \textit{NASA Formal Methods 2013}. Neuveden: Springer, 2013, p.~1-15. ISBN~978-3-642-38087-7. Available from: https://dx.doi.org/10.1007/978-3-642-38088-4\_{}1.
|