LTL Model Checking of LLVM Bitcode with Symbolic Data
| Authors | |
|---|---|
| Year of publication | 2014 |
| Type | Article in Proceedings |
| Conference | Proceedings of MEMICS'14 |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-319-14896-0_5 |
| Field | Informatics |
| Keywords | llvm; formal verification; model checking |
| Description | The correctness of parallel and reactive programs is often easier specified using formulae of temporal logics. Yet verifying that a system satisfies such specifications is more difficult than verifying safety properties: the recurrence of a specific program state has to be detected. This paper reports on the development of a generic framework for automatic verification of linear temporal logic specifications for programs in LLVM bitcode. Our method searches explicitly through all possible interleavings of parallel threads (control non-determinism) but represents symbolically the variable evaluations (data non-determinism), guided by the specification in order to prove the correctness. To evaluate the framework we compare our method with state-of-the-art tools on a set of unmodified C programs. |
| Related projects: |