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)

- 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

- ...(to be updated, meanwhile please consult the references in the papers above for more related work)
- Peter Selinger: Models for an Adversary-Centric Protocol Logic. Electronic Notes in Theoretical Computer Science Volume 55, Issue 1, January 2003, Pages 69-84 (correctenss of cryptographic protocols via finite models)
- J. Goubault-Larrecq. Finite Models for Formal Security Proofs. Journal of Computer Security 18(6), pages 1247-1299, 2010 (correctenss of cryptographic protocols via finite models; extraction of formally checkable proofs, e.g. in Coq)

#### parameterised cache coherence protocols (translations of EFSM models from the papers by Delzanno et al.)

#### lossy channel systems

- Alternating bit protocol (translation of the specification by Abdulla and Jonsson)
- ...

#### 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

- Token passing protocol for trees
- Two-way token passing protocol for trees (there are some insignificant typos in spec. To be corrected soon)

#### parameterized tree systems (specified by tree rewriting rules)

- Burn's mutual exclusion on PSO model (unsafe)
- Burn's mutual exclusion with fences on PSO model (safe)