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:
- Rich Counter-Examples for Temporal-Epistemic Logic Model Checking. Simon Busard, Charles Pecheur. Proceedings Second International Workshop on Interactions, Games and Protocols, Tallinn, Estonia, 25th March 2012.
Tags: -
Find It
Sections
Verification Diagnosis Autonomy ModelChecking Planning PDDL Requirements Testing LTL ThemeCoverage HumanComputerInteraction UserModel ProjectMOVES ThemeHMI LVL Website SymbolicModelChecking CTL Actions SMV EpistemicLogic ProjectNASA PartialOrderReduction BoundedModelChecking ThemePOR TemporalLogic Simulation Tools Tutorial Publication Equivalences