DIVINE 4.4

• Authors: ROČKAI Petr; LAUKO Henrich; ŠTILL Vladimír; BARANOVÁ Zuzana; KORENČIK Lukáš; MATOUŠEK Adam; BARNAT Jiří; ŠÁRNÍK Jakub; MRÁZEK Jan; KEJSTOVÁ Katarína; KUČERA Tadeáš
• Year of publication: 2021
• MU Faculty or unit: Faculty of Informatics

Web

• URL
• zdrojový kód

• Description: 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.

Related projects

• Automatizace formální verifikace