DIVINE: Explicit-State LTL Model Checker

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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	https://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:	Correctness Analysis of C and C++ Programs with Threads Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity