A CLP heap solver for test case generation

作者:Albert Elvira*; Garcia De La Banda Maria; Gomez Zamalloa Miguel; Miguel Rojas Jose; Stuckey Peter
来源:Theory and Practice of Logic Programming, 2013, 13(4-5): 721-735.
DOI:10.1017/S1471068413000458

摘要

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.

  • 出版日期2013-7