Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Qex: Symbolic SQL Query Explorer

Margus Veanes, Nikolai Tillmann, and Peli de Halleux

Abstract

We describe a technique and a tool called Qex for generating input tables and parameter values for a given parameterized SQL query. The evaluation semantics of an SQL query is translated into a specific background theory for a satisfiability modulo theories (SMT) solver as a set of equational axioms. Symbolic evaluation of a goal formula together with the background theory yields a model from which concrete tables and values are extracted. We use the SMT solver Z3 in the concrete implementation of Qex and provide an evaluation of its performance.

Details

Publication typeInproceedings
Published inLPAR-16
Pages425-446
Volume6355
SeriesLNAI
PublisherSpringer Verlag

Previous versions

Margus Veanes, Nikolai Tillmann, and Jonathan de Halleux. Qex: Symbolic SQL Query Explorer, Microsoft Research, October 2009.

> Publications > Qex: Symbolic SQL Query Explorer