| Identifikační kód | RIV/00216224:14330/13:00066525 |
|---|
| Název v anglickém jazyce | Improved State Space Reductions for LTL Model Checking of C & C++ Programs |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Petr Ročkai (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 1292358)
Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | model checking; C; C++; LTL; LLVM; DIVINE |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-38088-4_1 |
|---|