Reachability as Derivability, Finite Countermodels and Verification.

We propose a simple and efficient approach to the verification of parameterized and infinite state system. The approach is based on modeling the reachability relation between parameterized states as deducibility between suitable encodings of the states using formulae of first-order logic. To establish a safety property, namely the non-reachability of unsafe states, a finite model finder is used to generate a finite countermodel, thus providing the witness for non-deducibility. We show that under an appropriate encoding the combination of finite model finding and theorem proving provides us with a decision procedure for the safety of the lossy channel systems. We illustrate the approach by reporting on experiments verifying both alternating bit protocol (specified as a lossy channel system) and a number of parameterized cache coherence protocols specified by extended finite state machines. In these experiments, the finite model finder Mace4 is used. [ABSTRACT FROM AUTHOR]