ROČKAI, Petr, Jiří BARNAT a Luboš BRIM. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. In Guillaume Brat, Neha Rungta, Arnaud Venet. NASA Formal Methods 2013. Neuveden: Springer. s. 1-15. ISBN 978-3-642-38087-7. doi:10.1007/978-3-642-38088-4_1. 2013.
Další formáty:   BibTeX LaTeX RIS
Zá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
Originální 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-38088-4_1
Klíčová slova anglicky model checking; C; C++; LTL; LLVM; DIVINE
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2014 23:38.
Anotace
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 VaVNázev: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
MUNI/A/0760/2012, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 30. 3. 2024 08:42