Zde se nacházíte:
Informace o publikaci
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: |