Personal tools
You are here: Home Events Abstract Archives 2003 Proving Pointer Programs in Higher-Order Logic

Proving Pointer Programs in Higher-Order Logic

Tobias Nipkow Department of Computer Science Technical University of Munich 4pm Thursday 13 March 2003 Room 2511, JCMB, King's Buildings

Reasoning about pointer programs in Hoare logic is fairly straightforward in principle: simply regard the heap as a collection of variables mapping addresses to data. This idea goes back to Rod Burstall. We have implemented Hoare logic in the theorem prover Isabelle/HOL, extended it with a theory of pointers, and conducted a major case study to prove the viability of this approach: the verification of the Schorr-Waite garbage collection algorithm. I will explain the theoretical foundations, demonstrate some small examples, and talk about the Schorr-Waite case study.

This is joint work with Farhad Mehta.

Document Actions