TY - GEN
T1 - Boolean heaps
AU - Podelski, Andreas
AU - Wies, Thomas
PY - 2005
Y1 - 2005
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=33646065057&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33646065057&partnerID=8YFLogxK
U2 - 10.1007/11547662_19
DO - 10.1007/11547662_19
M3 - Conference contribution
AN - SCOPUS:33646065057
SN - 3540285849
SN - 9783540285847
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 268
EP - 283
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 12th International Symposium on Static Analysis, SAS 2005
Y2 - 7 September 2005 through 9 September 2005
ER -