Detailed Information on Publication Record
2012
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
BARNAT, Jiří, Luboš BRIM and Petr ROČKAIBasic information
Original name
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
Authors
BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution)
Edition
Berlin, NASA Formal Methods, p. 252-266, 15 pp. 2012
Publisher
Springer-Verlag Berlin Heidelberg
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
United States of America
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/12:00057345
Organization unit
Faculty of Informatics
ISBN
978-3-642-28890-6
ISSN
Keywords in English
Model checking; real code; DiVinE
Tags
International impact, Reviewed
Změněno: 23/4/2013 13:13, RNDr. Pavel Šmerk, Ph.D.
Abstract
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.
Links
| GAP202/11/0312, research and development project |
|