CLP Heap Solver
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.
We have developed a novel CLP heap solver for the test
case generation of heap-manipulating programs that is more
scalable than previous proposals (e.g. lazy initialization),
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.
Using our CLP Heap Solver
The CLP Heap Solver is available as a standalone Prolog
program. Some basic examples are provided and the user can also
write up heap-manipulating programs manually. Please read
the README file for a guide to the
use of the heap
solver.
Download CLP Heap
Solver v1.0 (tar file) (updated June 24, 2013)
Experimental Evaluation
The CLP Heap Solver has been integrated in the web
interface of PET. The following table allows the user to
run a set of benchmarks and compare the results obtained
by the standard execution of PET with no aliasing, the
execution of PET considering aliasing explicitly and the
execution of PET using the CLP Heap Solver.
| Benchmark |
PET Standard |
PET+Aliasing |
CLP Heap Solver |