Abstract

The Hoare formula P {Q} R had its 40th birthday this year! The ideas appearing in Hoare’s 1969 paper are the basis for program verification today, but now they are mechanised inside complex and sophisticated verification systems. I will compare automated methods for proving Hoare formulae based both on the forward computation of postconditions and on the backwards computation of preconditions. Although precondition methods are better known, I will argue the case for computing postconditions as this provides a verification spectrum ranging from symbolic execution (e.g. bounded model checking) to full proof of correctness.

My talk is a revised and extended version of what I presented at the recent Tony Hoare 75 birthday celebration event. I have made a few corrections and added some details on the semantic encoding in HOL .