Formal Methods Wiki
ProCoS II - Provably Correct Systems
EC stars
ProCoS II project

A ProCoS II Project Final Report: ESPRIT Basic Research project 7071, Jonathan Bowen (University of Reading), C.A.R. Hoare (Oxford University), Hans Langmaack (Christian-Albrechts-Universität Kiel), Ernst-Rüdiger Olderog (University of Oldenburg) and Anders P. Ravn (Technical University of Denmark). Bulletin of the European Association for Theoretical Computer Science (EATCS), Number 59, pages 76–99, June 1996.

A ProCoS tutorial on The ProCoS Approach to the Design of Real-Time Systems was presented at the FME'96 conference (Formal Methods Europe), Oxford, UK, 18–22 March 1996.

This document contains information relevant to the ESPRIT Basic Research ProCoS II project (no. 7071) on Provably Correct Systems. ProCoS II was a follow-on of the ProCoS I which finished on 23 October 1995. An associated Working Group continues until the end of 1996.

The project based its investigations around the occam and transputer' paradigm. A summary of the project published in the EATCS Bulletin (10 pages - also available in an automatically converted hypertext form) and another produced for a project review (13 pages) are available. A more technical overview (12 pages) of the project may also be found which includes a gas burner case study:

Diagram of gas burner

The ProCoS-WG Working Group was established during the project to help promulgation of project results and to gain feedback from Working Group members. ProCoS supported ZUM'94, ZUM'95 and the FTRTFT'94 meeting. A tutorial on the work of the ProCoS project with an associated 48 page survey paper entitled Provably Correct Systems and a 100 page tutorial handout was presented at the FTRTFT Symposium, September 1994.

Information on archives of online project documents and publications are available from ProCoS II sites:

A comprehensive searchable bibliography of project publications in BibTeX database format (for use with the LaTeX document preparation system) is also available, together with the bibliography for the original Technical Annex for the project.

Personnel involved with the ProCoS II project at Oxford include Tony Hoare who is the overall project manager and coordinator, He Jifeng who is working full-time on the project, and Jonathan Bowen (now leading the Formal Methods Group at the Department of Computer Scienbce, University of Reading) who is managing the associated ProCoS-WG Working Group. Other researchers associated with ProCoS include Gavin Lowe who is working on a related project. Stephen Brien has previously been associated with the project. Joan Arnold is the project secretary.

For further information please email and to join the postal and/or electronic mailing list, please send a request to At the OUCL, this list is gatewayed to the local newsgroup ox.comlab.procos.

See also:

Maintained by Jonathan Bowen as part of the ProCoS archive.
Comments and requests are welcome.