Formal Methods Wiki
ProCoS — Provably Correct Systems

ProCoS I project[]

This document contains information relevant to the ESPRIT ProCoS I project (no. 3104, 1989–1992) on Provably Correct Systems that was the forerunner of the ProCoS II project. The project based its investigations around the occam and transputer paradigm and ran from 1989 for 2½ years. A summary of the project plans was published at the start of the project:

A ProCoS Project Description: ESPRIT BRA 3104, Dines Bjørner, C.A.R. Hoare, Jonathan P. Bowen, He Jifeng, Hans Langmaack, Ernst-Rüdiger Olderog, Ursula Martin, Victoria Stavridou, Fleming Nielson, Hanne Riis Nielson, Howard Barringer, Doug Edwards, Hans Henrik Løvengreen, Anders Ravn and Hans Rischel. Bulletin of the European Association for Theoretical Computer Science (EATCS), 39, pages 60-73, October 1989.

The results of the project are available as a large technical report:

Dines Bjørner, Hans Langmaack and C.A.R. Hoare (eds.), Provably Correct Systems, ProCoS Technical Report [ID/DTH DB 13/1], Dept. of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, January 1993.

A published summary of ProCoS I produced at the end of the project is also available:

Dines Bjørner, Trusted computing systems, Proc. 14th International Conference on Software Engineering (ICSE), Melbourne, Australia, 11–14 May 1992 (North-Holland, 1992).

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