LTL Model Checking of LLVM Bitcode with Symbolic Data

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BAUCH Petr HAVEL Vojtěch BARNAT Jiří

Rok publikování 2014
Druh Článek ve sborníku
Konference Proceedings of MEMICS'14
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.