Boolean Heaps

10 years 6 months ago
Boolean Heaps
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 eps 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 an states (bitvectors). A program is abstracted to a program over boolean heaps. For each command of the program, the correspondract 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.
Andreas Podelski, Thomas Wies
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAS
Authors Andreas Podelski, Thomas Wies
Comments (0)