Proving Pointer Programs in Higher-Order Logic
Building on the work of Burstall, 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 higher-level 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. Apart from some smaller examples, 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 its readable
proof in Isabelle/HOL.
ps
doi:10.1016/j.ic.2004.10.007
BibTeX:
@article{MehtaN-IC05,author={Farhad Mehta and Tobias Nipkow},
title={Proving Pointer Programs in Higher-Order Logic},
journal={Information and Computation},
year=2005,volume=199,pages={200-227}}
The full proof of the Schorr-Waite algorithm
This is an extended version of the conference paper.