Heap assumptions on demand

Andreas Podelski, Andrey Rybalchenko, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 20th International Conference, CAV 2008, Proceedings
Number of pages14
StatePublished - 2008
Event20th International Conference on Computer Aided Verification, CAV 2008 - Princeton, NJ, United States
Duration: Jul 7 2008Jul 14 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5123 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other20th International Conference on Computer Aided Verification, CAV 2008
Country/TerritoryUnited States
CityPrinceton, NJ

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Heap assumptions on demand'. Together they form a unique fingerprint.

Cite this