Embedded Systems Group (ES)

Model Checking By Induction

This tool can be used to check whether a Kripke structure satisfies a given safety property by means of IC3 (Incremental Construction of Inductive Clauses for Indubitable Correctness) which is also called property directed reachability (PDR).

The syntax for the state transition system (the Kripke structure) should be obvious: First, you should list the variables 𝒱 known by the transition system. The transitions are given as a propositional logic formula over these variables 𝒱 and their values on the next state (denoted as next(x) for variable x∈𝒱). State sets as the initial states and the states of the property to be checked as safety property are given as propositional logic formulas over the variables 𝒱.

The tool will draw the transition system as an explicit state transition system and will then first perform some initial checks that include the simple induction rule. If these initial checks are not conclusive, PDR is applied to incrementally refine the assertion list until a counterexample is found or the assertion list allows an induction proof.

variables 𝒱:
Initial States 𝒥:
Transition Relation 𝓡:
Safety Property Φ: