Model Checking of C and C++ with DIVINE 4

• Autoři: BARANOVÁ Zuzana; BARNAT Jiří; KEJSTOVÁ Katarína; KUČERA Tadeáš; LAUKO Henrich; MRÁZEK Jan; ROČKAI Petr; ŠTILL Vladimír
• Rok publikování: 2017
• Druh: Článek ve sborníku
• Konference: Automated Technology for Verification and Analysis
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
• Doi: http://dx.doi.org/10.1007/978-3-319-68167-2_14
• Obor: Informatika
• Klíčová slova: Model Checking; Verification; C; C++; DIVINE
• Popis: The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

Související projekty

• Correctness Analysis of C and C++ Programs with Threads
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity