Title
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic
Abstract
Bornat has recently described an approach to reasoning about pointers, building on work of Morris. Here we describe a semantics that validates the approach, and use it to help deviseaxioms for operations that allocate and dispose of memory.1. INTRODUCTIONIt is widely acknowledged that pointers cause problems forprogram-proving formalisms (e.g. [8, 17, 13, 16, 9, 1, 14, 7]),but there is less agreement on precisely what the problemsare. So, before describing our own work, we rst...
Year
DOI
Venue
2000
10.1145/351268.351291
PPDP
Keywords
Field
DocType
pointer aliasing,semantic analysis,hoare logic,lambda calculus
Pointer (computer programming),Aliasing (computing),Lambda calculus,Programming language,Computer science,Axiom,Pointer aliasing,Hoare logic,Theoretical computer science,Explicit substitution,Semantics
Conference
ISBN
Citations 
PageRank 
1-58113-265-4
15
3.24
References 
Authors
13
3
Name
Order
Citations
PageRank
Cristiano Calcagno1153.24
Samin Ishtiaq214715.28
Peter W. O'hearn31861113.11