In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], 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, based on eager local searches constrained through control-flow loop detection. © 2013 Springer-Verlag.
CITATION STYLE
Ročkai, P., Barnat, J., & Brim, L. (2013). Improved state space reductions for LTL model checking of C and C++ programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7871 LNCS, pp. 1–15). https://doi.org/10.1007/978-3-642-38088-4_1
Mendeley helps you to discover research relevant for your work.