DIVINE: Explicit-State LTL Model Checker
Authors | |
---|---|
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 | |
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: |