Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

17

CADE
2003
Springer

favoriteEmaildiscussreport

174views Logical Reasoning» more CADE 2003»

Proving Pointer Programs in Higher-Order Logic

14 years 5 months ago

Proving Pointer Programs in Higher-Order Logic

Download www4.in.tum.de

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 higherlevel 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 present part of the readable proof in Isabelle/HOL.

Farhad Mehta, Tobias Nipkow

Real-time Traffic

Automated Reasoning | CADE 2003 | Graph Marking Algorithm | Non-trivial Case Study | Reasoning Methods |

claim paper

Related Content

» Separation Logic for HigherOrder Store

» HigherOrder Logic Programming as Constraint Logic Programming

» Adapting functional programs to higher order logic

» Termination and Reduction Checking for HigherOrder Logic Programs

» Tabling for HigherOrder Logic Programming

» HigherOrder and Modal Logic as a Framework for ExplanationBased Generalization

» A Complete Narrowing Calculus for HigherOrder Functional Logic Programming

» A Relational Modal Logic for HigherOrder Stateful ADTs

» Nested Hoare Triples and Frame Rules for HigherOrder Store

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2003
Where	CADE
Authors	Farhad Mehta, Tobias Nipkow

Comments (0)