Proving Pointer Programs in Higher-Order Logic

14 years 7 months ago
Proving Pointer Programs in Higher-Order Logic
This paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higherlevel data types for verification. The programming language is embedded in higher-order logic, its Hoare logic is derived. The whole development is purely definitional and thus sound. The viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr-Waite graph marking algorithm and present part of the readable proof in Isabelle/HOL.
Farhad Mehta, Tobias Nipkow
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Farhad Mehta, Tobias Nipkow
Comments (0)