Abstract
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 .
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
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)
Csallner, C., Smaragdakis, Y.: Check ’n’ Crash: combining static checking and testing. In: ICSE, pp. 422–431. ACM, New York (2005)
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)
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)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
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)
Dutertre, B., de Moura, L.: The YICES SMT solver. Technical report, Computer Science Laboratory, SRI International (2006), http://yices.csl.sri.com/tool-paper.pdf (visited July 2010)
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)
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)
Ghilardi, S.: Quantifier elimination and provers integration. Electr. Notes Theor. Comput. Sci. 86(1) (2003)
Gladisch, C.: Verification-based test case generation for full feasible branch coverage. In: SEFM, pp. 159–168 (2008)
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)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, London (2000)
KeY project homepage, http://www.key-project.org/
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)
Leavens, G., Cheon, Y.: Design by contract with JML (2006), http://www.eecs.ucf.edu/~leavens/JML/jmldbc.pdf (visited May 2010)
McMinn, P.: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab. 14(2), 105–156 (2004)
Moskal, M.: Satisfiability Modulo Software. PhD thesis, University of Wrocław (2009)
Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. Electr. Notes Theor. Comput. Sci. 198(2), 19–35 (2008)
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)
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)
Visser, W., Pǎsǎreanu, C., Khurshid, S.: Test input generation with Java PathFinder. In: ISSTA, pp. 97–107. ACM, New York (2004)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 IFIP International Federation for Information Processing
About this paper
Cite this paper
Gladisch, C.D. (2010). Test Data Generation for Programs with Quantified First-Order Logic Specifications. In: Petrenko, A., Simão, A., Maldonado, J.C. (eds) Testing Software and Systems. ICTSS 2010. Lecture Notes in Computer Science, vol 6435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16573-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-16573-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16572-6
Online ISBN: 978-3-642-16573-3
eBook Packages: Computer ScienceComputer Science (R0)