*** Reminder:FACS/LMS Evening Seminar by Prof Mike Gordon: Forward with Hoare, 1 December 2009, London Mathematical Society, Demorgan House

[paul...@googlemail.com]

(Apologies if you receive multiple copies of this announcement)

BCS-FACS Evening Seminar Series
Joint event with the London Mathematical Society

Forward with Hoare

Professor Mike Gordon, FRS
(Cambridge University)

1 December 2009

6pm

London Mathematical Society
De Morgan House
57-58 Russell Square
London WC1B 4HS
United Kingdom

Abstract

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 served from 5.30pm

The seminar is free of charge and open to everyone. If you would like
to attend, please email Paul Boca [paul...@googlemail.com] by
>>> 27 November 2009 <<< . Pre-registration is required.

FACS website: http://www.bcs-facs.org

LMS website: http://www.lms.ac.uk

Map of venue location: http://www.lms.ac.uk/contact/map.html