Improved State Space Reductions for LTL Model Checking of C & C++ Programs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066525" target="_blank" >RIV/00216224:14330/13:00066525 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-38088-4_1" target="_blank" >http://dx.doi.org/10.1007/978-3-642-38088-4_1</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-38088-4_1" target="_blank" >10.1007/978-3-642-38088-4_1</a>
Alternative languages
Result language
angličtina
Original language name
Improved State Space Reductions for LTL Model Checking of C & C++ Programs
Original language 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Software Components in Embedded Systems: Development and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
NASA Formal Methods 2013
ISBN
9783642380877
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
1-15
Publisher name
Springer
Place of publication
Neuveden
Event location
NASA Ames Research Center
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—