LTL Model Checking of LLVM Bitcode with Symbolic Data
| Autoři | |
|---|---|
| Rok publikování | 2014 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of MEMICS'14 |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-319-14896-0_5 |
| Obor | Informatika |
| Klíčová slova | llvm; formal verification; model checking |
| Popis | 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. |
| Související projekty: |