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 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. 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 presents part of the readable proof in Isabelle/HOL.
pdf
ps
BibTeX:
@inproceedings{MehtaN-CADE03,author={Farhad Mehta and Tobias Nipkow},
title={Proving Pointer Programs in Higher-Order Logic},
booktitle="Automated Deduction --- CADE-19",editor="F. Baader",
year=2003,publisher=Springer,series=LNCS,volume={2741},pages={121--135}}
The full proof of the Schorr-Waite algorithm
The extended journal version