Counterexamples in Symbolic Model Checking


An advantage of model checking is the capability to report a counter-example, i.e. an execution sequence violating the checked property. Most model checkers produce counter-examples, but they are generally only linear. We work on defining and combining solutions to improve the diagnostic information returned by symbolic model checkers. The main studied directions are trace annotation, the generation of branching counter-examples, the minimization of counter-examples and the identification of critical diagnostic information.

LVL Members: Simon Busard, Charles Pecheur

External Partners: None

Related Publications: