Proving Pointer Programs in Higher-Order Logic

Farhad Mehta and Tobias Nipkow

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

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