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

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

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

V originále

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