Heap assumptions on demand

Andreas Podelski, Andrey Rybalchenko, Thomas Wies

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

Abstract

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
Pages314-327
Number of pages14
DOIs
StatePublished - Aug 13 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

Other

Other20th International Conference on Computer Aided Verification, CAV 2008
CountryUnited States
CityPrinceton, NJ
Period7/7/087/14/08

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap assumptions on demand. In Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings (pp. 314-327). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5123 LNCS). https://doi.org/10.1007/978-3-540-70545-1_31