Proving pointer programs in higher-order logic

Farhad Mehta; Tobias Nipkow

doi:10.1016/j.ic.2004.10.007

Proving pointer programs in higher-order logic

Farhad Mehta, Tobias Nipkow

Default

ETH Zurich

Research output: Contribution to journal › Conference article › peer-review

49 Scopus citations

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.

Original language	English
Pages (from-to)	200-227
Number of pages	28
Journal	Information and Computation
Volume	199
Issue number	1-2
DOIs	https://doi.org/10.1016/j.ic.2004.10.007
State	Published - 25 May 2005
Event	19th International Conference on Automated Deduction (CADE-19) - Duration: 28 Jul 2003 → 28 Jul 2003

Keywords

Higher-order logic
Hoare logic
Pointer programs
Schorr-Waite algorithm
Verification

Access to Document

10.1016/j.ic.2004.10.007

Cite this

@article{2a0936eaec9a49ebbfe28618b948ac20,

title = "Proving pointer programs in higher-order logic",

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 = "Higher-order logic, Hoare logic, Pointer programs, Schorr-Waite algorithm, Verification",

author = "Farhad Mehta and Tobias Nipkow",

note = "Funding Information: ∗ Corresponding author. Fax: +41 44 632 1435. E-mail address: [email protected] (F. Mehta). 1 Work done while at the Technische Universit{\"a}t M{\"u}nchen, supported by DFG Grant NI 491/6-1.; 19th International Conference on Automated Deduction (CADE-19) ; Conference date: 28-07-2003 Through 28-07-2003",

year = "2005",

month = may,

day = "25",

doi = "10.1016/j.ic.2004.10.007",

language = "English",

volume = "199",

pages = "200--227",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Elsevier Inc.",

number = "1-2",

}

TY - JOUR

T1 - Proving pointer programs in higher-order logic

AU - Mehta, Farhad

AU - Nipkow, Tobias

N1 - Funding Information: ∗ Corresponding author. Fax: +41 44 632 1435. E-mail address: [email protected] (F. Mehta). 1 Work done while at the Technische Universität München, supported by DFG Grant NI 491/6-1.

PY - 2005/5/25

Y1 - 2005/5/25

N2 - 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.

AB - 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.

KW - Higher-order logic

KW - Hoare logic

KW - Pointer programs

KW - Schorr-Waite algorithm

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=20144375380&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2004.10.007

DO - 10.1016/j.ic.2004.10.007

M3 - Conference article

AN - SCOPUS:20144375380

SN - 0890-5401

VL - 199

SP - 200

EP - 227

JO - Information and Computation

JF - Information and Computation

IS - 1-2

T2 - 19th International Conference on Automated Deduction (CADE-19)

Y2 - 28 July 2003 through 28 July 2003

ER -

Proving pointer programs in higher-order logic

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this