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 a Jiří BARNAT

Základní údaje

Originální název

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

Autoři

ROČKAI, Petr (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, garant, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Neuveden, Software Engineering and Formal Methods, od s. 268-282, 15 s. 2015

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/15:00081181

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-22968-3

ISSN

DOI

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

UT WoS

000365046400019

Klíčová slova anglicky

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

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 20:49, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA15-08772S, projekt VaV

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

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

ROČKAI, Petr, Vladimír ŠTILL a 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, s. 268-282. ISBN 978-3-319-22968-3. Dostupné z: 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 a 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, s.~268-282. ISBN~978-3-319-22968-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-22969-0\_{}19.

Podrobný výpis o publikaci