ProCoS

Provably Correct Systems (ProCoS)
Type of projectCollaborative research
ProductsComputer science research
Duration Calculus
LocationEurope
Key peopleTony Hoare
Dines Bjørner
Hans Langmaack
Ernst-Rüdiger Olderog
Established1 May 1989 (1989-05-01)
Disestablished1997
FundingEuropean Strategic Programme on Research in Information Technology (ESPRIT) Framework Programmes for Research and Technological Development
StatusFinished
Websitearchive.comlab.ox.ac.uk/procos

ProCoS ("Provably Correct Systems") was a European ESPRIT initiative of two collaborative computer science research projects and a Working Group, with further associated international liaison funding, started in 1989 and ending in 1997.

The projects aimed to connect computer-based systems in a formal manner at different levels of abstraction, including requirements, specifications, programs, through compilation, to machine code, and even directly into hardware described by netlists, based around the occam programming language and the Transputer processor. A major research output of the project was Duration Calculus by Zhou Chaochen, Tony Hoare, and Anders P. Ravn. A later result of the project was Unifying Theories of Programming (UTP) by Tony Hoare and He Jifeng.

Projects and grants

The following projects and associated collaborations were funded:

Partners

The main project partners, among others, were:

A two-day reunion meeting was held at the BCS London office in March 2015.

References

  1. 1 2 3 Bowen, Jonathan P.; Fränzle, Martin; Olderog, Ernst-Rüdiger; Bjørner, Dines; Hansen, Michael R.; Langmaack, Hans; Liu, Zhiming; Martin, Ursula (2026). "Experiences from the European ProCoS Projects: Provably Correct Systems". Formal Aspects of Computing. 38. doi:10.1145/3803555.
  2. ↑ "PROCOS – Grant agreement ID: 3104". CORDIS. European Union: European Commission. 19 August 1994. Retrieved 28 April 2026.
  3. ↑ Bjørner, D. (2017). "ProCoS: How It All Began – as Seen from Denmark". In Hinchey, M.; Bowen, J.P.; Olderog, E-R. (eds.). Provably Correct Systems. NASA Monographs in Systems and Software Engineering. Cham: Springer. pp. 3–5. doi:10.1007/978-3-319-48628-4_1.
  4. ↑ "PROCOS II – Grant agreement ID: 7071". CORDIS. European Union: European Commission. 17 June 1994. Retrieved 28 April 2026.
  5. ↑ "PROCOS – Grant agreement ID: 8694". CORDIS. European Union: European Commission. 21 June 1994. Retrieved 28 April 2026.
  6. 1 2 Bowen, Jonathan; Hoare, C.A.R.; Langmaack, Hans; Olderog, Ernst-Rüdiger; Ravn, Anders P. (1998). "A ProCoS-WG Working Group Final Report: ESPRIT Working Group 8694" (PDF). Bulletin of the European Association for Theoretical Computer Science. 64: 63–72. Retrieved 26 April 2026.
  7. ↑ Bjørner, Dines. "ProCoS – Provably Correct Systems". Orbit. Denmark: DTU. Retrieved 26 April 2026.
  8. ↑ Langmaack, H. (1997). "The ProCoS Approach to Correct Systems". Real-Time Systems. 13: 253–275. doi:10.1023/A:1007963427189.
  9. ↑ Olderog, Ernst-Rüdiger. "ProCoS: Provably Correct Systems". Germany: University of Oldenburg. Retrieved 26 April 2026.
  10. ↑ Hinchey, M.; Bowen, J.P.; Olderog, E-R., eds. (2017). Provably Correct Systems. NASA Monographs in Systems and Software Engineering. Cham: Springer. doi:10.1007/978-3-319-48628-4. ISBN 978-3-319-48627-7.