BCS-FACS Evening Seminar -- Joint event with the London Mathematical Society,
Tuesday 1 December 2009, 5.45pm

Professor Michael J.C. Gordon (University of Cambridge)
Forward with Hoare

Hoare's celebrated paper entitled "An Axiomatic Basis for Computer Programming" appeared in 1969, so the Hoare formula P{S}Q is now forty years old! That paper introduced Hoare Logic, which is still the basis for program verification today, but is now mechanised inside sophisticated verification systems. My talk aims to give an accessible introduction to 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, computing postconditions provides a verification framework that encompasses methods ranging from symbolic execution to full deductive proof of correctness.

Refreshments will be available from 5.30pm.

The seminar will be held at De Morgan House, 57-58 Russell Square, London WC1B 4HS. Underground: Russell Square or Holborn. For a map see here.

The seminar is free of charge and open to everyone. If you would like to attend, please email Paul Boca [Paul.Boca@googlemail.com]. Information is also available on the BCS-FACS website.