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 Calcagno | 1 | 15 | 3.24 |
Samin Ishtiaq | 2 | 147 | 15.28 |
Peter W. O'hearn | 3 | 1861 | 113.11 |