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: |