DIVINE 4.4

ROČKAI, Petr, Henrich LAUKO, Vladimír ŠTILL, Zuzana BARANOVÁ, Lukáš KORENČIK, Adam MATOUŠEK, Jiří BARNAT, Jakub ŠÁRNÍK, Jan MRÁZEK, Katarína KEJSTOVÁ a Tadeáš KUČERA. DIVINE 4.4. 2021.

Základní údaje

• Originální název: DIVINE 4.4
• Autoři: ROČKAI, Petr (703 Slovensko, garant, domácí), Henrich LAUKO (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, domácí), Zuzana BARANOVÁ (703 Slovensko), Lukáš KORENČIK (703 Slovensko), Adam MATOUŠEK (203 Česká republika), Jiří BARNAT (203 Česká republika), Jakub ŠÁRNÍK (203 Česká republika), Jan MRÁZEK (203 Česká republika), Katarína KEJSTOVÁ (703 Slovensko) a Tadeáš KUČERA (203 Česká republika).
• Vydání: 2021.

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: URL zdrojový kód
• Kód RIV: RIV/00216224:14330/21:00119996
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: model checking; correctness; analysis; concurrency; symbolic
• Technické parametry: n/a
• Příznaky: Mezinárodní význam

Anotace

DIVINE is a modern, multi-paradigm model checker and incorporates both explicit and symbolic methods, along with abstraction. Based on the LLVM toolchain, it can verify programs written in multiple real-world programming languages, including C and C++. The verification core is built on a foundation of high­-per­for­mance algorithms and data structures.

Návaznosti

• TH04010192, projekt VaV: Název: Automatizace formální verifikace (Akronym: AUFOVER)

Investor: Technologická agentura ČR, Automatizace formální verifikace