DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky DiVinE 3.0 -- Explicitně-stavový nástroj pro ověřování modelu pro vícevláknové C a C++ programy
Autoři

BARNAT Jiří BRIM Luboš HAVEL Vojtěch HAVLÍČEK Jan KRIHO Jan LENČO Milan ROČKAI Petr ŠTILL Vladimír WEISER Jiří

Rok publikování 2013
Druh Článek ve sborníku
Konference Computer Aided Verification 2013
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-39799-8_60
Obor Informatika
Klíčová slova model checking; LLVM; C++; C; LTL; timed automata
Popis We present a new release of the parallel and distributed LTL model checker DIVINE. The major improvements in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DIVINE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools.
Související projekty:

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