Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Článek ve sborníku |
| Konference | NASA Formal Methods |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-642-28891-3_25 |
| Obor | Informatika |
| Klíčová slova | Model checking; real code; DiVinE |
| Popis | 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. |
| Související projekty: |