Verification via countermodel finding
We propose a simple but powerful approach to the verification of parameterised systems.
The approach is based on modelling the reachability between parameterized states as deducibility
between suitable encodings of states by formulae of first-order predicate logic. To establish a safety
property, that is non-reachability of unsafe states, the finite model finder is used to find a
finite countermodel, the witness for non-deducibility.
A short paper with Appendices reporting on experiments (draft)
Reachability as deducibility, finite countermodels and verification
Even shorter variant of this paper has appeared in Pre-proceedings of AVOCS'09 (short papers)
Further development of the Finite Countermodels Method (FCM) has been presented in:
- A. Lisitsa: Finite Model Finding for Parameterized Verification CoRR abs/1011.0447:
(2010)
(FCM is at least as powerful sa regular model checking and the methods based on monotone abstractions for linear systems)
- A. Lisitsa: Reachability as
Derivability, Finite Countermodels and Verification. ATVA 2010: 233-244
(Decision procedure for lossy channel systems based on FCM; Verficiation of counting abtsractions of parameterized cache coherence protocols)
- A. Lisitsa: Finite countermodels for safety verification of
parameterized tree systems CoRR abs/1107.5142: (2011)
(FCM is at least as powerful as regular tree model checking and the methods based on monotone abstractions for tree systems)
- A. Lisitsa: First-order finite satisfiability vs tree automata in safety verification CoRR
abs/1107.0349: (2011)
(FCM is at least as powerful as tree autiomata completion techniques)
- A. Lisitsa: Finite Models vs Tree
Automata in Safety Verification. RTA 2012: 225-239
(FCM is at least as powerful as tree automata completion techniques; rewriting modulo theory; a conference version of the above paper)
-
A.Lisitsa: Finite Reasons for Safety, Journal of Automated Reasoning, Feb 2013,
Online First
Talks
Related work
First-order translations of the protocols specifications and correctness conditions in
Prover9/Mace4 syntax
parameterised cache coherence protocols (translations of EFSM models from the papers by Delzanno et al.)
lossy channel systems
parameterized linear arrays of automata
- Mutual exclusion (translation of the
specification by Abdulla,Delzanno and Rezine)
regular model checking problems
- Passing token protocol (non-optimized translation, where the transition is presented by an explicit finite state transducer)
- Parameterized Bakery mutual exclusion protocol (translation of the specification given by Nilsson)
- Peterson- (incomplete translation (one rule is off) of the specification of parameterized Peterson protocol by Fisman and Pnueli; I conjecture that the verification of the full specification can not be done with FCM)
- ...
regular tree model checking problems
parameterized tree systems (specified by tree rewriting rules)
weak memory models
Last updated 20.05.2013