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

March 3, 2020

We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement 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.

This work has been partially supported by the Czech Science Foundation grant No. GAP202/11/0312.

Authors: Jiří BarnatLuboš BrimVojtěch HavelJan HavlíčekJan KrihoMilan LenčoPetr RočkaiVladimír Štill, and Jiří Weiser

Project: DIVINE4

Published in: Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868.

Go to pdf

Article Link


Partner University



Associated Research Projects