Sciweavers

CAV
2008
Springer

Heap Assumptions on Demand

13 years 5 months ago
Heap Assumptions on Demand
Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interween counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate xamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.
Andreas Podelski, Andrey Rybalchenko, Thomas Wies
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Andreas Podelski, Andrey Rybalchenko, Thomas Wies
Comments (0)