Formal Methods Wiki

Project information[]

This archive contains information relevant to the collaborative UK IED (Information Engineering Directorate) DTI / SERC safemos project, which ran for 3½ years at OUCL from 1989 to 1993.

The project partners were:


The safemos project used formal methods extensively, and HOL and Z in particular.

The project liaised extensively with the European ESPRIT ProCoS project since both projects had similar goals and a common partner in the Oxford University Computing Laboratory. C.A.R. Hoare and Jonathan Bowen were joint principal investigators at Oxford.

In later collaboration between Oxford and Cambridge after the formal end of the project, an attempt has been made to investigate the support of Z using HOL. The source files are available.

Project publications[]

A book entitled Towards Verified Systems, largely on the work of the project, is available (published October 1994). The table of contents and preface are available online.

An overview paper on the work of the project is also available online:

Jonathan Bowen, He Jifeng, Roger Hale and John Herbert, Towards Verified Systems: The SAFEMOS Project. In C. Mitchell and V. Stavridou (eds.), The Mathematics of Dependable Systems, Oxford University Press, The Institute of Mathematics and its Applications Conference Series, volume 55, pages 23–48, 1995.

See also safemos project entries in the on-line bibliography for the related ProCoS II project.

Subsequent projects[]

Jonathan Bowen subsequently worked on a continuation project investigating Provably Correct Hardware/Software Co-design that started immediately after the end of the safemos project. This is still closely connected with ProCoS, including an associated Working Group, as well as the Hardware Compilation Group at OUCL.

From 1st October 1995, Jonathan Bowen was a lecturer at the Department of Computer Science, University of Reading. In March 2000, he joined London South Bank University as Professor of Computing.

For further information, please contact Jonathan Bowen.