Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
Alexei Lisitsa · EPiC series in computing · 2018
We present a case study of the verification of parameterized mutual exclusion protocol using finite model finder Mace4. Thhe verification follows an approach based on modeling of reachability between states of the protocol as deducibility between appropriate encodings of states by first-order predicate logic formulae. The result of successful verification is a finite countermodel, a witness of non-deducibility, which represents a system invariant.