\input zb-basic
\input zb-ioport
\iteman{io-port 06069207}
\itemau{Barnat, Ji\v{r}i; Brim, Lubo\v{s}; Ro\v{c}kai, Petr}
\itemti{Towards LTL model checking of unmodified thread-based C \& C++ programs.}
\itemso{Goodloe, Alwyn E. (ed.) et al., NASA formal methods. 4th international symposium, NFM 2012, Norfolk, VA, USA, April 3--5, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28890-6/pbk). Lecture Notes in Computer Science 7226, 252-266 (2012).}
\itemab
Summary: 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-28891-3\_25}
\end