Skip to main content
SpringerLink
Log in

Symbolic Query Exploration

  • Conference paper
Book cover Formal Methods and Software Engineering (ICFEM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5885))

Included in the following conference series:

Abstract

We study the problem of generating a database and parameters for a given parameterized SQL query satisfying a given test condition. We introduce a formal background theory that includes arithmetic, tuples, and sets, and translate the generation problem into a satisfiability or model generation problem modulo the background theory. We use the satisfiability modulo theories (SMT) solver Z3 in the concrete implementation. We describe an application of model generation in the context of the database unit testing framework of Visual Studio.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. SELECT (T-SQL), http://msdn.microsoft.com/en-us/library/ms189499.aspx

  2. Binnig, C., Kossmann, D., Lo, E., Özsu, M.T.: Qagen: generating query-aware test databases. In: SIGMOD 2007: Proceedings of the 2007 ACM SIGMOD international conference on Management of data, pp. 341–352. ACM, New York (2007)

    Chapter  Google Scholar 

  3. Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307–321. Springer, Heidelberg (2009)

    Google Scholar 

  4. Boyer, R.S., Moore, J.S.: A computational logic handbook. Academic Press Professional, Inc., San Diego (1988)

    MATH  Google Scholar 

  5. Chakravarthy, U.S., Grant, J., Minker, J.: Logic-based approach to semantic query optimization. ACM Trans. Database Syst. 15(2), 162–207 (1990)

    Article  Google Scholar 

  6. Chays, D., Shahid, J., Frankl, P.G.: Query-based test generation for database applications. In: Proceedings of the 1st International Workshop on Testing Database Systems (DBTest 2008), pp. 1–6. ACM, New York (2008)

    Chapter  Google Scholar 

  7. Chinaei, H.R.: An ordered bag semantics of SQL. Master’s thesis, University of Waterloo, Waterloo, Ontario, Canada (2007)

    Google Scholar 

  8. Cook, B., Kröning, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 296–300. Springer, Heidelberg (2005)

    Google Scholar 

  9. Dantsin, E., Voronkov, A.: Complexity of query answering in logic databases with complex values. In: Adian, S., Nerode, A. (eds.) LFCS 1997. LNCS, vol. 1234, pp. 56–66. Springer, Heidelberg (1997)

    Google Scholar 

  10. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Deng, Y., Frankl, P., Chays, D.: Testing database transactions with AGENDA. In: ICSE 2005: Proceedings of the 27th international conference on Software engineering, pp. 78–87. ACM, New York (2005)

    Chapter  Google Scholar 

  12. Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: Proceedings of the 2007 International Symposium on Software Testing and Analysis (ISSTA 2007), pp. 151–162. ACM, New York (2007)

    Google Scholar 

  13. Jackson, D.: Automating first-order relational logic. SIGSOFT Softw. Eng. Notes 25(6), 130–139 (2000)

    Article  Google Scholar 

  14. Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)

    Google Scholar 

  15. Khalek, S.A., Elkarablieh, B., Laleye, Y.O., Khurshid, S.: Query-aware test generation using a relational constraint solver. In: ASE, pp. 238–247 (2008)

    Google Scholar 

  16. Negri, M., Pelagatti, G., Sbattella, L.: Formal semantics of SQL queries. ACM Transactions on Database Systems 17(3), 513–534 (1991)

    Article  MathSciNet  Google Scholar 

  17. Pex, http://research.microsoft.com/projects/pex

  18. Qex, http://research.microsoft.com/projects/qex

  19. Sheard, T., Stemple, D.: Automatic verification of database transaction safety. ACM Trans. Database Syst. 14(3), 322–368 (1989)

    Article  Google Scholar 

  20. Tillmann, N., de Halleux, J.: Pex - white box test generation for .NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Tsai, W.T., Volovik, D., Keefe, T.F.: Automated test case generation for programs specified by relational algebra queries. IEEE Trans. Softw. Eng. 16(3), 316–324 (1990)

    Article  Google Scholar 

  22. Veanes, M., Bjørner, N.: Symbolic bounded conformance checking of model programs. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) Perspectives of System Informatics (PSI 2009). LNCS. Springer, Heidelberg (2009)

    Google Scholar 

  23. Veanes, M., Bjørner, N., Gurevich, Y., Schulte, W.: Symbolic bounded model checking of abstract state machines. Int. J. Software Informatics 3(2-3), 149–170 (2009)

    Google Scholar 

  24. Veanes, M., Grigorenko, P., de Halleux, P., Tillmann, N.: Symbolic query exploration. Technical Report MSR-TR-2009-65, Microsoft Research (May 2009)

    Google Scholar 

  25. Z3, http://research.microsoft.com/projects/z3

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Margus Veanes, Peli de Halleux & Nikolai Tillmann

  2. Institute of Cybernetics, Tallinn University of Technology, Tallinn, Estonia

    Pavel Grigorenko

Authors
  1. Margus Veanes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pavel Grigorenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peli de Halleux
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nikolai Tillmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Coordenadora da Engenharia de Computação, Diretora de Publicações da SBC, Depto. Informática, ontifícia Universidade Católica do Rio de Janeiro, ,, R. Marques de Sao Vicente 225 - Prédio do RDC - Sala 416, Rio de Jan,  

    Karin Breitman

  2. Department of Computer Science, University of York, ,, Heslington, YO10 5DD, York, UK,

    Ana Cavalcanti

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Veanes, M., Grigorenko, P., de Halleux, P., Tillmann, N. (2009). Symbolic Query Exploration. In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10373-5_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10372-8

  • Online ISBN: 978-3-642-10373-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation