Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9656884 | Information and Computation | 2005 | 28 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Farhad Mehta, Tobias Nipkow,