Techniques for Memory-Efficient Model Checking of C and C++ Code
| Autoři | |
|---|---|
| Rok publikování | 2015 |
| Druh | Článek ve sborníku |
| Konference | Software Engineering and Formal Methods |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-319-22969-0_19 |
| Obor | Informatika |
| Klíčová slova | LLVM; model checking; compression; memory-efficient; explicit-state |
| Popis | 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 storage in 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. |
| Související projekty: |