2013
Improved State Space Reductions for LTL Model Checking of C & C++ Programs
ROČKAI, Petr, Jiří BARNAT a Luboš BRIMZákladní údaje
Originální název
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 (703 Slovensko, domácí), Jiří BARNAT (203 Česká republika, garant, domácí) a Luboš BRIM (203 Česká republika, domácí)
Vydání
Neuveden, NASA Formal Methods 2013, od s. 1-15, 15 s. 2013
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Německo
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/13:00066525
Organizační jednotka
Fakulta informatiky
ISBN
978-3-642-38087-7
ISSN
Klíčová slova anglicky
model checking; C; C++; LTL; LLVM; DIVINE
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 27. 4. 2014 23:38, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
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.
Návaznosti
| GAP202/11/0312, projekt VaV |
| ||
| MUNI/A/0760/2012, interní kód MU |
|