Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

Silvio Ghilardi
(Università degli Studi di Milano)
Elena Pagani
(Università degli Studi di Milano)

Quite often, verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by a specifically designed technique for second order quantifier elimination. Our method, once applied to specifications of verification problems for parameterized distributed systems, produces integer variables systems that are ready to be model-checked by current SMT-based tools. We demonstrate the feasibility of the approach with a prototype implementation and first experiments.

In Catherine Dubois and Bruno Woltzenlogel Paleo: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 2017), Brasília, Brazil, 23-24 September 2017, Electronic Proceedings in Theoretical Computer Science 262, pp. 39–53.
Published: 4th December 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: