Explicit State Model Checking with DIVINE

VCLA and WPI will host a talk by Petr Rockai on December 6th, 2013.

ABSTRACT

DIVINE is a modern explicit-state model checker. The model checking core offers multiple algorithms, some of them suitable for parallel and/or distributed-memory verification. DIVINE also ships with a number of frontend components for different input languages. A major focus of the recent 3.x release series is a new LLVM-based frontend, which is suitable for model checking of closed, multi-threaded C and C++ programs. Both safety and LTL properties are supported. State space reductions make DIVINE a practical tool for model checking of real software components, and it has been successfully applied to parts of its own codebase. Full support for C++ (including exception handling and C++11) is provided by using a standard compiler to generate LLVM IR which is then verified.

The talk will give an overview of DIVINE, its history, current status and main features. Main part of the talk will focus on the LLVM component, its accompanying reductions and how suitable LLVM IR is obtained from C and C++ programs. The talk will include a short demonstration.