The development of FDR and FDR2 has received support from a number of sources.
The initial goals of the Formal Systems refinement checker were outlined by Inmos Ltd, and an early version of the system was developed in collaboration with them. The research and development of FDR1 was further funded in part by the US Office of Naval Research (contract N00014-87-J1242), and ESPRIT project 2701 (PUMA).
The development of the second generation tools described here was funded in part from internal resources, and also by contributions under contracts from the United Kingdom Defence Research Agency, ONR project N00014-93-C-0213, and as part of ESPRIT project 7267 (OMI/STANDARDS).
The research at Oxford University forming the basis of A Syntax Reference was also funded under ONR contract N00014-87-J-1242. However, work beyond this research, including the `compilation' technique which closes off process terms to produce a finite-state transition system and operations defined over such trees necessary to perform normalisation, compression and refinement-checks were all funded by Formal Systems as part of the development of FDR and so remain the property of that company. Formal Systems is happy to discuss possible research projects with both academic and commercial organisations.
This document draws together material from a number of authors, principally: Paul Gardiner, Michael Goldsmith, Jason Hulance, David Jackson, Bill Roscoe and Bryan Scattergood.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.