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Á and Tadeáš KUČERA. DIVINE 4.4. 2021.

Basic information

• Original name: DIVINE 4.4
• Authors: ROČKAI, Petr (703 Slovakia, guarantor, belonging to the institution), Henrich LAUKO (703 Slovakia, belonging to the institution), Vladimír ŠTILL (203 Czech Republic, belonging to the institution), Zuzana BARANOVÁ (703 Slovakia), Lukáš KORENČIK (703 Slovakia), Adam MATOUŠEK (203 Czech Republic), Jiří BARNAT (203 Czech Republic), Jakub ŠÁRNÍK (203 Czech Republic), Jan MRÁZEK (203 Czech Republic), Katarína KEJSTOVÁ (703 Slovakia) and Tadeáš KUČERA (203 Czech Republic).
• Edition: 2021.

Other information

• Original language: English
• Type of outcome: Software
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL zdrojový kód
• RIV identification code: RIV/00216224:14330/21:00119996
• Organization unit: Faculty of Informatics
• Keywords in English: model checking; correctness; analysis; concurrency; symbolic
• Technical parameters: n/a
• Tags: International impact

Abstract

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.

Links

• TH04010192, research and development project: Name: Automatizace formální verifikace (Acronym: AUFOVER)

Investor: Technology Agency of the Czech Republic