COMPUTER CONSERVATION SOCIETY

      Seminar, Director's Suite, Science Museum, London SW7, UK
                      2pm, Tuesday 5 June 2001

                  PROGRAM VERIFICATION AND SEMANTICS
                          The Early Work

Co-chairs:
Prof Jonathan Bowen (South Bank University)
Prof Cliff Jones (Newcastle University)

The ability to prove mathematically that a program correctly implements its
specification is increasingly important in ensuring that high integrity
computer-based systems for security and safety-critical applications perform
correctly. Alan Turing was an early advocate of the need for appropriate
techniques, and Britain has from the beginning been at the forefront of
research developing new approaches to this area of computer science. The
formal verification of a program involves proving (in some way) the program's
consistency with a formal specification. To do this, the meaning of the
program also needs to be defined and understood. Thus it is necessary to
provide a precise mathematical semantics for constructs of the programming
language.

In this seminar, a number of pioneers will present some of their early
experiences of the field. Participants will include:

   Prof Sir Tony Hoare (Queens University Belfast, Oxford U & Microsoft)
   Prof Robin Milner (Edinburgh & Cambridge U's)
   Prof Peter Landin (Queen Mary College London)
   Joe Stoy  (Oxford University Computing Lab)

The contributions will range from formal presentations to personal reminiscences.

Directions: the nearest tube station is South Kensington. Follow signs through
the underground walkway north to the museum (c5 minutes walk). The Science
Museum is on Exhibition Road.

Enquiries to George Davis 020 8681 7784   [log in to unmask]
--
Chris Burton - A member of the Computer Conservation Society
Tel and fax +44(0)1691 791 274