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
Volume5123 LNCS
DOIs
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Heap
Shape Analysis
Precondition
Termination
Counterexample
Aliasing
Reachability
Assertion
Sharing
Eliminate
Express
Experiments
Prototype
Demand
Experiment

ASJC Scopus subject areas

  • Biochemistry, Genetics and Molecular Biology(all)
  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap assumptions on demand. In Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings (Vol. 5123 LNCS, 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

Heap assumptions on demand. / Podelski, Andreas; Rybalchenko, Andrey; Wies, Thomas.

Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings. Vol. 5123 LNCS 2008. p. 314-327 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5123 LNCS).

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

Podelski, A, Rybalchenko, A & Wies, T 2008, Heap assumptions on demand. in Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings. vol. 5123 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5123 LNCS, pp. 314-327, 20th International Conference on Computer Aided Verification, CAV 2008, Princeton, NJ, United States, 7/7/08. https://doi.org/10.1007/978-3-540-70545-1_31
Podelski A, Rybalchenko A, Wies T. Heap assumptions on demand. In Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings. Vol. 5123 LNCS. 2008. p. 314-327. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-70545-1_31
Podelski, Andreas ; Rybalchenko, Andrey ; Wies, Thomas. / Heap assumptions on demand. Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings. Vol. 5123 LNCS 2008. pp. 314-327 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ccd2ea2a731a428f97544d3d87228954,
title = "Heap assumptions on demand",
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.",
author = "Andreas Podelski and Andrey Rybalchenko and Thomas Wies",
year = "2008",
doi = "10.1007/978-3-540-70545-1_31",
language = "English (US)",
isbn = "3540705430",
volume = "5123 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "314--327",
booktitle = "Computer Aided Verification - 20th International Conference, CAV 2008, Proceedings",

}

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

VL - 5123 LNCS

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

ER -