Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{979265,
author = {Barnat, Jiří and Brim, Luboš and Ročkai, Petr},
address = {Berlin},
booktitle = {NASA Formal Methods},
doi = {http://dx.doi.org/10.1007/978-3-642-28891-3_25},
keywords = {Model checking; real code; DiVinE},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Berlin},
isbn = {978-3-642-28890-6},
pages = {252-266},
publisher = {Springer-Verlag Berlin Heidelberg},
title = {Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs},
year = {2012}
}
TY - JOUR
ID - 979265
AU - Barnat, Jiří - Brim, Luboš - Ročkai, Petr
PY - 2012
TI - Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
PB - Springer-Verlag Berlin Heidelberg
CY - Berlin
SN - 9783642288906
KW - Model checking
KW - real code
KW - DiVinE
N2 - 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.
ER -
BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C \&{} C++ Programs. In \textit{NASA Formal Methods}. Berlin: Springer-Verlag Berlin Heidelberg, 2012, s.~252-266. ISBN~978-3-642-28890-6. Dostupné z: https://dx.doi.org/10.1007/978-3-642-28891-3\_{}25.
|
