---
OA_type: closed access
_id: '4366'
abstract:
- lang: eng
  text: 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.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Andreas
  full_name: Podelski, Andreas
  last_name: Podelski
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
- first_name: Thomas
  full_name: Wies, Thomas
  id: 447BFB88-F248-11E8-B48F-1D18A9856A87
  last_name: Wies
citation:
  ama: 'Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: <i>Proceedings
    of the 30th International Conference of Computer Aided Verifacation</i>. Vol 5123.
    Springer Nature; 2008:314-327. doi:<a href="https://doi.org/10.1007/978-3-540-70545-1_31">10.1007/978-3-540-70545-1_31</a>'
  apa: 'Podelski, A., Rybalchenko, A., &#38; Wies, T. (2008). Heap Assumptions on
    Demand. In <i>Proceedings of the 30th international conference of computer aided
    verifacation</i> (Vol. 5123, pp. 314–327). Princeton, NJ, United Stated: Springer
    Nature. <a href="https://doi.org/10.1007/978-3-540-70545-1_31">https://doi.org/10.1007/978-3-540-70545-1_31</a>'
  chicago: Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions
    on Demand.” In <i>Proceedings of the 30th International Conference of Computer
    Aided Verifacation</i>, 5123:314–27. Springer Nature, 2008. <a href="https://doi.org/10.1007/978-3-540-70545-1_31">https://doi.org/10.1007/978-3-540-70545-1_31</a>.
  ieee: A. Podelski, A. Rybalchenko, and T. Wies, “Heap Assumptions on Demand,” in
    <i>Proceedings of the 30th international conference of computer aided verifacation</i>,
    Princeton, NJ, United Stated, 2008, vol. 5123, pp. 314–327.
  ista: 'Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. Proceedings
    of the 30th international conference of computer aided verifacation. CAV: Computer
    Aided Verification, Lecture Notes in Computer Science, vol. 5123, 314–327.'
  mla: Podelski, Andreas, et al. “Heap Assumptions on Demand.” <i>Proceedings of the
    30th International Conference of Computer Aided Verifacation</i>, vol. 5123, Springer
    Nature, 2008, pp. 314–27, doi:<a href="https://doi.org/10.1007/978-3-540-70545-1_31">10.1007/978-3-540-70545-1_31</a>.
  short: A. Podelski, A. Rybalchenko, T. Wies, in:, Proceedings of the 30th International
    Conference of Computer Aided Verifacation, Springer Nature, 2008, pp. 314–327.
conference:
  end_date: 2008-07-14
  location: Princeton, NJ, United Stated
  name: 'CAV: Computer Aided Verification'
  start_date: 2008-07-07
date_created: 2018-12-11T12:08:29Z
date_published: 2008-07-07T00:00:00Z
date_updated: 2026-05-28T13:24:39Z
day: '07'
doi: 10.1007/978-3-540-70545-1_31
extern: '1'
intvolume: '      5123'
language:
- iso: eng
month: '07'
oa_version: None
page: 314 - 327
publication: Proceedings of the 30th international conference of computer aided verifacation
publication_identifier:
  eisbn:
  - '9783540705451'
  isbn:
  - '9783540705437'
publication_status: published
publisher: Springer Nature
publist_id: '1091'
status: public
title: Heap Assumptions on Demand
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 5123
year: '2008'
...