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

D 2015

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

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

Basic information

Original name

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

Authors

ROČKAI, Petr (703 Slovakia, belonging to the institution), Vladimír ŠTILL (203 Czech Republic, guarantor, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)

Edition

Neuveden, Software Engineering and Formal Methods, p. 268-282, 15 pp. 2015

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00081181

Organization unit

Faculty of Informatics

ISBN

978-3-319-22968-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-22969-0_19

UT WoS

000365046400019

Keywords in English

LLVM; model checking; compression; memory-efficient; explicit-state

Abstract

V originále

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.

Links

GA15-08772S, research and development project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

MUNI/A/1159/2014, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masaryk University, Category A

Citovat

ROČKAI, Petr, Vladimír ŠTILL and Jiří BARNAT. Techniques for Memory-Efficient Model Checking of C and C++ Code. In Radu Calinescu, Bernhard Rumpe. Software Engineering and Formal Methods. Neuveden: Springer International Publishing, 2015, p. 268-282. ISBN 978-3-319-22968-3. Available from: https://dx.doi.org/10.1007/978-3-319-22969-0_19.

@inproceedings{1316721,
   author = {Ročkai, Petr and Štill, Vladimír and Barnat, Jiří},
   address = {Neuveden},
   booktitle = {Software Engineering and Formal Methods},
   doi = {http://dx.doi.org/10.1007/978-3-319-22969-0_19},
   editor = {Radu Calinescu, Bernhard Rumpe},
   keywords = {LLVM; model checking; compression; memory-efficient; explicit-state},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-22968-3},
   pages = {268-282},
   publisher = {Springer International Publishing},
   title = {Techniques for Memory-Efficient Model Checking of C and C++ Code},
   year = {2015}
}

TY  - JOUR
ID  - 1316721
AU  - Ročkai, Petr - Štill, Vladimír - Barnat, Jiří
PY  - 2015
TI  - Techniques for Memory-Efficient Model Checking of C and C++ Code
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319229683
KW  - LLVM
KW  - model checking
KW  - compression
KW  - memory-efficient
KW  - explicit-state
N2  - 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.
ER  -

ROČKAI, Petr, Vladimír ŠTILL and Jiří BARNAT. Techniques for Memory-Efficient Model Checking of C and C++ Code. In Radu Calinescu, Bernhard Rumpe. \textit{Software Engineering and Formal Methods}. Neuveden: Springer International Publishing, 2015, p.~268-282. ISBN~978-3-319-22968-3. Available from: https://dx.doi.org/10.1007/978-3-319-22969-0\_{}19.

Detailed Information on Publication Record