Other formats:
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 and 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, p.~252-266. ISBN~978-3-642-28890-6. Available from: https://dx.doi.org/10.1007/978-3-642-28891-3\_{}25.
|