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

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2013
Type Article in Proceedings
Conference Computer Aided Verification 2013
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-39799-8_60
Field Informatics
Keywords model checking; LLVM; C++; C; LTL; timed automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info