DIVINE 3.0

ROČKAI, Petr, Jiří BARNAT, Vladimír ŠTILL, Jiří WEISER, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK a Jan KRIHO. DIVINE 3.0. 2013.

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

• Originální 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í
• WWW: zdrojový kód URL
• 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.

Anotace

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++.