2012
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
BARNAT, Jiří, Luboš BRIM a Petr ROČKAIZákladní údaje
Originální název
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
Autoři
BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí)
Vydání
Berlin, NASA Formal Methods, od s. 252-266, 15 s. 2012
Nakladatel
Springer-Verlag Berlin Heidelberg
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Spojené státy
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/12:00057345
Organizační jednotka
Fakulta informatiky
ISBN
978-3-642-28890-6
ISSN
Klíčová slova anglicky
Model checking; real code; DiVinE
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 23. 4. 2013 13:13, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
In this paper we present a new approach to verification of multi-threaded C/C++ programs. Our solution effectively chains the parallel and distributed-memory model checker DiVinE with CLang and the LLVM bitcode interpreter. This combination offers full LTL, distributed-memory model checking of virtually unmodified C/C++ source code and is supported by a newly introduced path-reduction technique. We demonstrate the efficiency of the reduction and also the capacity to produce human-readable counter-examples in two small case studies: a C implementation of the Peterson's mutual exclusion protocol and a C++ implementation of a shared-memory, lock-free FIFO data structure designed for fast inter-thread communication.
Návaznosti
| GAP202/11/0312, projekt VaV |
|