ProCoS
| Provably Correct Systems (ProCoS) | |
|---|---|
 | |
| Type of project | Collaborative research |
| Products | Computer science research Duration Calculus |
| Location | Europe |
| Key people | Tony Hoare Dines Bjørner Hans Langmaack Ernst-Rüdiger Olderog |
| Established | 1 May 1989 |
| Disestablished | 1997 |
| Funding | European Strategic Programme on Research in Information Technology (ESPRIT) Framework Programmes for Research and Technological Development |
| Status | Finished |
| Website | archive.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:
- ESPRIT ProCoS BRA (Basic Research Action) project (no. 3104, 1989–1992)
- ESPRIT ProCoS II project (no. 7071, 1992–1995)
- ESPRIT ProCoS-WG Working Group (no. 8694, 1994–1997)
- UK EPSRC Provably Correct Hardware/Software Co-design project (1993–1996)
- ESPRIT/NSF ProCoS-US (EC-US027, 1993–1997) European/United States travel grant on Provably Correct Hardware Compilation
- ESPRIT KIT (Keep in Touch) travel grant (1993–1996) with Zhou Chaochen, UNU-IIST (Macau)
- ESPRIT PROCORSYS KIT (Keep in Touch) travel grant (KIT 142, 1994–1997) with Augusto Sampaio, Departamento de Informatica, Universidade Federal de Pernambuco (Brazil)
- UK EPSRC Visiting Fellowship (1996–1997) to study Provably Correct Real-Time Systems for Michael Schenke, Oldenburg University (Germany)
Partners
The main project partners, among others, were:
- Technical University of Denmark – DTU (Denmark)
- Kiel University (Germany)
- University of Oldenburg (Germany)
- University of Oxford (United Kingdom)
A two-day reunion meeting was held at the BCS London office in March 2015.
