Boolean heaps

Andreas Podelski, Thomas Wies

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

Abstract

We show that the idea of predicates on heap objects can be cast in the framework of predicate abstraction. This leads to an alternative view on the underlying concepts of three-valued shape analysis by Sagiv, Reps and Wilhelm. Our construction of the abstract post operator is analogous to the corresponding construction for classical predicate abstraction, except that predicates over objects on the heap take the place of state predicates, and boolean heaps (sets of bitvectors) take the place of boolean states (bitvectors). A program is abstracted to a program over boolean heaps. For each command of the program, the corresponding abstract command is effectively constructed by deductive reasoning, namely by the application of the weakest precondition operator and an entailment test. We thus obtain a symbolic framework for shape analysis.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages268-283
Number of pages16
DOIs
StatePublished - 2005
Event12th International Symposium on Static Analysis, SAS 2005 - London, United Kingdom
Duration: Sep 7 2005Sep 9 2005

Publication series

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

Other

Other12th International Symposium on Static Analysis, SAS 2005
CountryUnited Kingdom
CityLondon
Period9/7/059/9/05

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Boolean heaps'. Together they form a unique fingerprint.

  • Cite this

    Podelski, A., & Wies, T. (2005). Boolean heaps. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 268-283). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3672 LNCS). https://doi.org/10.1007/11547662_19