DIVINE: Explicit-State LTL Model Checker

Logo poskytovatele

Varování

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

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

Rok publikování 2016
Druh Článek ve sborníku
Konference Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www 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
Obor Informatika
Klíčová slova DIVINE model checker; LTL model checking
Popis 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.
Související projekty:

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