![Důležité termíny](https://cdn.muni.cz/media/3633704/image_2.jpg?mode=crop¢er=0.5,0.5&rnd=133572412150000000&heightratio=0.5&width=278)
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: |