Techniques for Memory-Efficient Model Checking of C and C++ Code

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ROČKAI Petr ŠTILL Vladimír BARNAT Jiří

Year of publication 2015
Type Article in Proceedings
Conference Software Engineering and Formal Methods
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.