Heap assumptions on demand

Abstract. Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reach-ability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique inter-play between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.