DIVINE 3.0
Identifikátory výsledku
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
—
Alternativní jazyky
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++.
Klasifikace
Druh
R - Software
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach
Ostatní
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ů
Údaje specifické pro druh výsledku
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