Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-18T00:47:57.721Z Has data issue: false hasContentIssue false
  • English
  • Français

A CLP heap solver for test case generation

Published online by Cambridge University Press:  25 September 2013

ELVIRA ALBERT ,
MARÍA GARCÍA DE LA BANDA ,
MIGUEL GÓMEZ-ZAMALLOA ,
JOSÉ MIGUEL ROJAS  and
PETER STUCKEY
ELVIRA ALBERT
Affiliation:
DSIC, Complutense University of Madrid (UCM), E-28040 Madrid, Spain
MARÍA GARCÍA DE LA BANDA
Affiliation:
Monash University, Australia IMDEA Software, Madrid, Spain
MIGUEL GÓMEZ-ZAMALLOA
Affiliation:
DSIC, Complutense University of Madrid (UCM), E-28040 Madrid, Spain
JOSÉ MIGUEL ROJAS
Affiliation:
DLSIIS, Technical University of Madrid (UPM), E-28660 Boadilla del Monte, Madrid, Spain
PETER STUCKEY
Affiliation:
National ICT Australia, and University of Melbourne, Australia IMDEA Software, Madrid, Spain
Get access Rights & Permissions [Opens in a new window]

Abstract

One of the main challenges to software testing today is to efficiently handle heap-manipulating programs. These programs often build complex, dynamically allocated data structures during execution and, to ensure reliability, the testing process needs to consider all possible shapes these data structures can take. This creates scalability issues since high (often exponential) numbers of shapes may be built due to the aliasing of references. This paper presents a novel CLP heap solver for the test case generation of heap-manipulating programs that is more scalable than previous proposals, thanks to the treatment of reference aliasing by means of disjunction, and to the use of advanced back-propagation of heap related constraints. In addition, the heap solver supports the use of heap assumptions to avoid aliasing of data that, though legal, should not be provided as input.

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 13 , Special Issue 4-5: 29th International Conference on Logic Programming , July 2013 , pp. 721 - 735
Copyright
Copyright © 2013 [ELVIRA ALBERT, MARÍA GARCÍA DE LA BANDA, MIGUEL GÓMEZ-ZAMALLOA, JOSÉ MIGUEL ROJAS, and PETER STUCKEY] 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ammann, P. and Offutt, J. 2008. Introduction to Software Testing. Cambridge University Press, Cambridge, UK.CrossRefGoogle Scholar
Charreteur, F., Botella, B. and Gotlieb, A. 2009. Modelling dynamic memory management in constraint-based testing. Journal of Systems and Software 82, 11, 1755–1766.CrossRefGoogle Scholar
Degrave, F., Schrijvers, T. and Vanhoof, W. 2010. Towards a framework for constraint-based test case generation. In LOPSTR'09, LNCS 6037, Springer, 128–142.Google Scholar
Gómez-Zamalloa, M., Albert, E. and Puebla, G. 2009. Decompilation of Java bytecode to prolog by partial evaluation. Information and Software Technology 51, 10, 1409–1427.CrossRefGoogle Scholar
Gómez-Zamalloa, M., Albert, E. and Puebla, G. 2010. Test case generation for object-oriented imperative languages in CLP. Theory and Practice of Logic Programming, ICLP'10 Special Issue 10, 4–6, 659–674.CrossRefGoogle Scholar
Goodrich, M., Tamassia, R. and Zamore, R. 2003. The net.datastructures Package, version 3. URL: http://net3.datastructures.net.Google Scholar
Gotlieb, A., Botella, B. and Rueher, M. 2000. A CLP framework for computing structural test data. In CL'00, LNAI 1861, Springer, 399–413.Google Scholar
Khurshid, S., Pǎsǎreanu, C. S. and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In TACAS'03, LNCS 2619, Springer, 553–568.Google Scholar
King, J. C. 1976. Symbolic execution and program testing. Communications of the ACM 19, 7, 385–394.CrossRefGoogle Scholar
Meudec, C. 2001. ATGen: Automatic test data generation using constraint logic programming and symbolic execution. Software Testing, Verification & Reliability 11, 2, 81–96.CrossRefGoogle Scholar
Müller, R. A., Lembeck, C. and Kuchen, H. 2004. A symbolic java virtual machine for test case generation. In IASTEDSE'04, ACTA Press, 365–371.Google Scholar
Offutt, A. J. and Liu, S. 1999. Generating test data from SOFL specifications. Journal of Systems and Software 49, 1, 49–62.CrossRefGoogle Scholar
Peleska, J., Vorobev, E. and Lapschies, F. 2011. Automated test case generation with SMT-Solving and abstract interpretation. In NFM'11, LNCS 6617, Springer, 298–312.Google Scholar
Podelski, A., Rybalchenko, A. and Wies, T. 2008. Heap assumptions on demand. In CAV'08, LNCS 5123, Springer, 314–327.Google Scholar
Pǎsǎreanu, C. S. and Rungta, N. 2010. Symbolic PathFinder: Symbolic execution of Java bytecode. In ASE'10, ACM, 179–180.CrossRefGoogle Scholar
Pǎsǎreanu, C. S. and Visser, W. 2009. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer 11, 4, 339–353.CrossRefGoogle Scholar
Tillmann, N. and de Halleux, J. 2008. Pex: White box test generation for .NET. In TAP'08, LNCS 4966, Springer, 134–153.Google Scholar
Visser, W., Pǎsǎreanu, C. S. and Khurshid, S. 2004. Test input generation with Java PathFinder. In ISSTA'04, ACM, 97–107.CrossRefGoogle Scholar
Wielemaker, J. 2010. The SWI-Prolog User's Manual 5.9.9. URL: http://www.swiprolog.org.Google Scholar