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

• Název česky: Redukce stavového prostoru pro LTL ověřování modelu programů C a C++
• Autoři: ROČKAI Petr; BARNAT Jiří; BRIM Luboš
• Rok publikování: 2013
• Druh: Článek ve sborníku
• Konference: NASA Formal Methods 2013
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/978-3-642-38088-4_1
• Obor: Informatika
• Klíčová slova: model checking; C; C++; LTL; LLVM; DIVINE
• Popis: 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.

Související projekty

• Software Components in Embedded Systems: Development and Verification
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.