| Identifikační kód | RIV/00216224:14330/15:00081181 |
|---|
| Název v anglickém jazyce | Techniques for Memory-Efficient Model Checking of C and C++ Code |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2015 |
|---|
| 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)
Vladimír Štill (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6284272)
Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792) |
|---|
| Popis výsledku v anglickém jazyce | We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs. As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untime-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storagein a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty. |
|---|
| Klíčová slova oddělená středníkem | LLVM; model checking; compression; memory-efficient; explicit-state |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-319-22969-0_19 |
|---|