Qex: symbolic SQL query explorer. 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.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Veanes, Margus; Bjørner, Nikolaj: Foundations of finite symbolic tree transducers (2011)
- Clarke, Edmund M. (ed.); Voronkov, Andrei (ed.): Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers (2010)
- Veanes, Margus; Tillmann, Nikolai; de Halleux, Jonathan: Qex: symbolic SQL query explorer (2010)