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