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

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2015
Druh Článek ve sborníku
Konference Software Engineering and Formal Methods
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.