EJCP 2015

Model Checking Modulo Theories


This lecture is an introduction to Model Checking Modulo Theories (MCMT), an new model checking technique invented by Silvio Ghilardi and Silvio Ranise. This technique is based on the integration of SMT solving and backward reachability. We will illustrate the concepts of MCMT with Cubicle, an open source model checker for verifying safety properties of array-based systems, a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. This lecture will also introduce the main concepts behind the construction of SMT solvers.


Files used during the demos: