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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066526" target="_blank" >RIV/00216224:14330/13:00066526 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_60" target="_blank" >http://dx.doi.org/10.1007/978-3-642-39799-8_60</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_60" target="_blank" >10.1007/978-3-642-39799-8_60</a>

Result language
angličtina
Original language name
DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
Original language 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 witharbitrary system modelling tools.
Czech name
—
Czech description
—

Project
<a href="/en/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Software Components in Embedded Systems: Development and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)