DIVINE 3.0

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00072941" target="_blank" >RIV/00216224:14330/13:00072941 - isvavai.cz</a>
Výsledek na webu
<a href="http://anna.fi.muni.cz/software.html#divine-3.0" target="_blank" >http://anna.fi.muni.cz/software.html#divine-3.0</a>
DOI - Digital Object Identifier
—

Jazyk výsledku
angličtina
Název v původním jazyce
DIVINE 3.0
Popis výsledku v původním jazyce
DIVINE is a modern explicit-state model checker. Building on high-performance algorithms and data structures, it offers unparalleled versatility, scaling from a typical developer?s laptop, up to a high-end compute cluster. What more, it can verify awide range of languages, including C and C++.
Název v anglickém jazyce
DIVINE 3.0
Popis výsledku anglicky
DIVINE is a modern explicit-state model checker. Building on high-performance algorithms and data structures, it offers unparalleled versatility, scaling from a typical developer?s laptop, up to a high-end compute cluster. What more, it can verify awide range of languages, including C and C++.

Rok uplatnění
2013
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Interní identifikační kód produktu
DIVINE 3.0
Technické parametry
Nástroj pro realizaci verifikace metodou ověřování modelu pro formule LTL (LTL Model Checking) v prostředí s distribuovanou pamětí s podporou redukce velikosti stavového prostoru metodou částečného uspořádání a s podporou ranné detekce chybného běhu. Oproti předchozím verzím je nástroj schopen přímo verifikovat zdrojové kódy C a C++, s možností snadného rozšíření na další programovací jazyky.
Ekonomické parametry
Nástroj slouží mimo jiné ke snížení nákladů na ověřování korektnosti softwareových systémů, a to částečnou automatizací procesů náročných na kvalifikovanou práci. Úspory zatím nelze kvantifikovat.
IČO vlastníka výsledku
00216224
Název vlastníka
Masarykova Univerzita

Podobné výsledky(10)