Improved State Space Reductions for LTL Model Checking of C & C++ Programs

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ROČKAI Petr BARNAT Jiří BRIM Luboš

Year of publication 2013
Type Article in Proceedings
Conference NASA Formal Methods 2013
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-38088-4_1
Field Informatics
Keywords model checking; C; C++; LTL; LLVM; DIVINE
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.