BCS Computer Conservation Society (CCS) & Formal Aspects of Computing Science (FACS) Specialist Groups

2pm Thursday, 2 December 2004, a Seminar, Director's Suite, Science Museum, Exhibition Road, London SW7 2DD, UK

See programme and photographs below. See also the notice in the BCS Computer Bulletin. See also a separate report of the meeting by Teresa Numerico and Jonathan P. Bowen. This has appeared as:

Numerico, T. and Bowen, J. P., Program Verification and Semantics: Further Work, Science Museum, London, FACS FACTS, Issue 2005-1, pages 18-25, March 2005.

Numerico, T. and Bowen, J. P., Program Verification and Semantics: Further Work, Science Museum, London. IEEE Annals of the History of Computing, 27(2), April-June 2005. In Events and Sightings, Chigusa Kita (ed.), pages 79-81.

Program Verification and Semantics: Further Work

Prof. Jonathan Bowen (London South Bank University, UK)
Prof. Cliff Jones (University of Newcastle upon Tyne, UK)
Dr. Teresa Numerico (London South Bank University, UK)

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 follow-on from a seminar in 2001, a number of computing pioneers presented some of their experiences of the field. The following spoke:

Prof. John C. Reynolds (Carnegie Mellon University, USA)
Prof. Gordon Plotkin (University of Edinburgh, UK)
Prof. Cliff Jones (University of Newcastle upon Tyne, UK)

The contributions ranged 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 and the entrance to the Director's Suite is just to the north of the main entrance and next to the Post Office. See visitor information and local map. All welcome, no booking necessary.

Programme

2.00 Introduction (Roger Johnson, Chair CCS)
2.05 John Reynolds (see paper)
3.00 Gordon Plotkin

3.55 Tea/coffee break (Sponsored by BCS-FACS)

Session 2 - Chair: Jonathan Bowen

4.30 Cliff Jones (see slides)
5.25 Concluding remarks
5.30 Close of meeting

Presentations lasted 40-45 minutes with good time for discussion and questions after each.

The meeting was open to all, with no booking required (subject to a seating limitation of around 100 people). 74 people signed the register. Attendees are encouraged to join CCS and/or FACS if you enjoyed the event, to help support future activities by these two BCS Specialist Groups. Paul Boca, the BCS-FACS membership secretary was be on hand during the (free!) tea/coffee break. Please contact Paul Boca if you would like to join FACS (cost £15 per annum for members of BCS and sister organizations, £30 otherwise).

Photographs

John Reynolds

Gordon Plotkin

Cliff Jones

Plotkin, Jones and Reynolds

See further photographs by Jonathan Bowen.

Virtual Museum of Computing