LTL Model Checking of LLVM Bitcode with Symbolic Data

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BAUCH Petr HAVEL Vojtěch BARNAT Jiří

Year of publication 2014
Type Article in Proceedings
Conference Proceedings of MEMICS'14
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.