Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic

Cristiano Calcagno, Samin Ishtiaq and Peter W. O'Hearn

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

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 devise axioms for operations that allocate and dispose of memory.