Test Data Generation for Programs with Quantified First-Order Logic Specifications

  • Christoph D. Gladisch
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6435)


We present a novel algorithm for test data generation that is based on techniques used in formal software verification. Prominent examples of such formal techniques are symbolic execution, theorem proving, satisfiability solving, and usage of specifications and program annotations such as loop invariants. These techniques are suitable for testing of small programs, such as, e.g., implementations of algorithms, that have to be tested extremely well.

In such scenarios test data is generated from test data constraints which are first-order logic formulas. These constraints are constructed from path conditions, specifications, and program annotation describing program paths that are hard to be tested randomly. A challenge is, however, to solve quantified formulas. The presented algorithm is capable of solving quantified formulas that state-of-the-art satisfiability modulo theory (SMT) solvers cannot solve. The algorithm is integrated in the formal verification and test generation tool KeY .


Dynamic Logic Proof Obligation Symbolic Execution Core Atom Test Data Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)Google Scholar
  3. 3.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Csallner, C., Smaragdakis, Y.: Check ’n’ Crash: combining static checking and testing. In: ICSE, pp. 422–431. ACM, New York (2005)Google Scholar
  5. 5.
    de Moura, L.M., 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)CrossRefGoogle Scholar
  6. 6.
    Deng, X., Robby, Hatcliff, J.: Kiasan/KUnit: Automatic test case generation and analysis feedback for open object-oriented systems. In: TAICPART-MUTATION 2007: Proceedings of the Testing: Academic and Industrial Conference Practice and Research Techniques - MUTATION, Washington, DC, USA, pp. 3–12. IEEE Computer Society, Los Alamitos (2007)CrossRefGoogle Scholar
  7. 7.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)CrossRefMathSciNetGoogle Scholar
  8. 8.
    du Bousquet, L., Ledru, Y., Maury, O., Oriat, C., Lanet, J.-L.: Case study in JML-based software validation. In: Proceedings Automated Software Engineering, pp. 294–297. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  9. 9.
    Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, Computer Science Laboratory, SRI International (2006), (visited July 2010)
  10. 10.
    Engel, C., Gladisch, C., Klebanov, V., Rümmer, P.: Integrating verification and testing of object-oriented software. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 182–191. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Ghilardi, S.: Quantifier elimination and provers integration. Electr. Notes Theor. Comput. Sci. 86(1) (2003)Google Scholar
  13. 13.
    Gladisch, C.: Verification-based test case generation for full feasible branch coverage. In: SEFM, pp. 159–168 (2008)Google Scholar
  14. 14.
    Gladisch, C.: Could we have chosen a better loop invariant or method contract? In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 74–89. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, London (2000)zbMATHGoogle Scholar
  16. 16.
    KeY project homepage,
  17. 17.
    Kiniry, J.R., Morkan, A.E., Denby, B.: Soundness and completeness warnings in ESC/Java2. In: Proc. Fifth Int. Workshop Specification and Verification of Component-Based Systems, pp. 19–24 (2006)Google Scholar
  18. 18.
    Leavens, G., Cheon, Y.: Design by contract with JML (2006), (visited May 2010)
  19. 19.
    McMinn, P.: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab. 14(2), 105–156 (2004)CrossRefGoogle Scholar
  20. 20.
    Moskal, M.: Satisfiability Modulo Software. PhD thesis, University of Wrocław (2009)Google Scholar
  21. 21.
    Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. Electr. Notes Theor. Comput. Sci. 198(2), 19–35 (2008)CrossRefMathSciNetGoogle Scholar
  22. 22.
    Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Challenges in satisfiability modulo theories. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 2–18. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  24. 24.
    Visser, W., Pǎsǎreanu, C., Khurshid, S.: Test input generation with Java PathFinder. In: ISSTA, pp. 97–107. ACM, New York (2004)CrossRefGoogle Scholar
  25. 25.
    Zhang, J., Zhang, H.: Extending finite model searching with congruence closure computation. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 94–102. Springer, Heidelberg (2004)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2010

Authors and Affiliations

  • Christoph D. Gladisch
    • 1
  1. 1.Department of Computer ScienceUniversity of Koblenz-LandauGermany

Personalised recommendations