Quantifier Elimination for Database Driven Verification

TL;DR

This paper explores the use of quantifier elimination and covers in database-driven verification, relating them to model theory and demonstrating practical computation methods within the Superposition Calculus.

Contribution

It introduces a novel connection between covers and model completions, and develops a constrained Superposition Calculus approach for efficient cover computation.

Findings

Covers are computationally tractable for application-specific language fragments.

Preliminary results show effectiveness on data-aware process benchmarks.

The approach is integrated into the MCMT verification tool.

Abstract

Running verification tasks in database driven systems requires solving quantifier elimination problems of a new kind. These quantifier elimination problems are related to the notion of a cover introduced in ESOP 2008 by Gulwani and Musuvathi. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus, equipped with appropriate settings and reduction strategies. In addition, we show that cover computations are computationally tractable for the fragment of the language used in applications to database driven verification. This observation is confirmed by analyzing the preliminary results obtained using the MCMT tool on the verification of data-aware process benchmarks. These benchmarks can be found in the last version of the tool distribution.