Techniques for Memory-Efficient Model Checking of C and C++ Code
| Authors | |
|---|---|
| Year of publication | 2015 |
| Type | Article in Proceedings |
| Conference | Software Engineering and Formal Methods |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-319-22969-0_19 |
| Field | Informatics |
| Keywords | LLVM; model checking; compression; memory-efficient; explicit-state |
| Description | 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. |
| Related projects: |