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:


Fibonacci Challenge!

Related work

First-order translations of the protocols specifications and correctness conditions in Prover9/Mace4 syntax

  • weak memory models

    Last updated 20.05.2013