BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg, 2012, p. 252-266. ISBN 978-3-642-28890-6. Available from: https://dx.doi.org/10.1007/978-3-642-28891-3_25.
Other formats:   BibTeX LaTeX RIS
Basic 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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-28891-3_25
Keywords in English Model checking; real code; DiVinE
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 23/4/2013 13:13.
Abstract
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 projectName: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
PrintDisplayed: 27/4/2024 00:05