DIVINE: Explicit-State LTL Model Checker

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

ŠTILL Vladimír ROČKAI Petr BARNAT Jiří

Year of publication 2016
Type Article in Proceedings
Conference Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
MU Faculty or unit

Faculty of Informatics

Citation
web http://dx.doi.org/10.1007/978-3-662-49674-9_60
Doi http://dx.doi.org/10.1007/978-3-662-49674-9_60
Field Informatics
Keywords DIVINE model checker; LTL model checking
Description DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.
Related projects:

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