Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

TL;DR

This paper introduces a logical technique for counter abstractions in distributed system verification, enabling the use of SMT tools through second-order quantifier elimination, supported by a prototype and initial experiments.

Contribution

It provides a novel logical foundation for counter simulations using second-order quantifier elimination, facilitating verification with existing SMT tools.

Findings

Feasibility demonstrated with prototype implementation.

Initial experiments show practical applicability.

Method produces integer variable systems suitable for model checking.

Abstract

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.