TY - GEN
T1 - Heap assumptions on demand
AU - Podelski, Andreas
AU - Rybalchenko, Andrey
AU - Wies, Thomas
PY - 2008
Y1 - 2008
N2 - 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 interplay 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.
AB - 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 interplay 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.
UR - http://www.scopus.com/inward/record.url?scp=48949104016&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=48949104016&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-70545-1_31
DO - 10.1007/978-3-540-70545-1_31
M3 - Conference contribution
AN - SCOPUS:48949104016
SN - 3540705430
SN - 9783540705437
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 314
EP - 327
BT - Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings
T2 - 20th International Conference on Computer Aided Verification, CAV 2008
Y2 - 7 July 2008 through 14 July 2008
ER -