Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
| Authors | |
|---|---|
| Year of publication | 2012 |
| Type | Article in Proceedings |
| Conference | NASA Formal Methods |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-642-28891-3_25 |
| Field | Informatics |
| Keywords | Model checking; real code; DiVinE |
| Description | 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. |
| Related projects: |