DIVINE: Explicit-State LTL Model Checker

• Autoři: ŠTILL Vladimír; ROČKAI Petr; BARNAT Jiří
• Rok publikování: 2016
• Druh: Článek ve sborníku
• Konference: Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://dx.doi.org/10.1007/978-3-662-49674-9_60
• Doi: http://dx.doi.org/10.1007/978-3-662-49674-9_60
• Obor: Informatika
• Klíčová slova: DIVINE model checker; LTL model checking
• Popis: DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.

Související projekty

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