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

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.