R 2013

DIVINE 3.0

ROČKAI, Petr, Jiří BARNAT, Vladimír ŠTILL, Jiří WEISER, Luboš BRIM et. al.

Základní údaje

Originální název

DIVINE 3.0

Autoři

ROČKAI, Petr (703 Slovensko, domácí), Jiří BARNAT (203 Česká republika, garant, domácí), Vladimír ŠTILL (203 Česká republika, domácí), Jiří WEISER (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Vojtěch HAVEL (203 Česká republika, domácí), Jan HAVLÍČEK (203 Česká republika, domácí) a Jan KRIHO (203 Česká republika, domácí)

Vydání

2013

Další údaje

Jazyk

angličtina

Typ výsledku

Software

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Kód RIV

RIV/00216224:14330/13:00072941

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

distributed-memory computing; LTL model checking; Partial Order Reduction; On-The-Fly verification; LLVM; Software Model Checking

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.
Změněno: 23. 4. 2014 12:49, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

V originále

DIVINE is a modern explicit-state model checker. Building on high­-per­for­mance algorithms and data structures, it offers unparalleled versatility, sca­ling from a typical developer’s laptop, up to a high-end compute cluster. What more, it can verify a wide range of languages, including C and C++.