Proving pointer programs in higher-order logic |
| |
Authors: | Farhad Mehta Tobias Nipkow |
| |
Affiliation: | aDepartment of Computer Science, ETH Zürich, Switzerland;bInstitut für Informatik, Technische Universität München, Germany |
| |
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. |
| |
Keywords: | Pointer programs Verification Hoare logic Higher-order logic Schorr– Waite algorithm |
本文献已被 ScienceDirect 等数据库收录! |