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.