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:

Activities

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. Prof. C.A.R. Hoare and Jonathan Bowen were joint principal investigators at Oxford.

In more recent further collaboration between Oxford and Cambridge since 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 on-line.

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

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 has been a lecturer at the Department of Computer Science, University of Reading.

Maintained as part of the ProCoS archive.
Comments and requests concerning safemos are welcome.

For further information, please contact Jonathan Bowen.