| EPSRC Reference: |
GR/L03071/01 |
| Title: |
AUTOMATIC GUIDENCE OF MECHANICALLY GENERATED PROOFS |
| Principal Investigator: |
Gordon, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 1996 |
Ends: |
30 September 1999 |
Value (£): |
198,783
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The use of formal methods of system development brings highly desirable benefits of reliability, safety and security of IT projects. Unfortunately, their exploitation by industry is hampered by the high skill levels and long development times which are required when using existing tools. Proof planning, as embodies in the CLaM system, has been successful in automating significant parts of the proof obligations required informal methods. We intend to interface CLaM to the HOL system, which is a formal method support tool used in universities, government and industry. In this way we hope to reduce skill levels and development time, making formal methods commercially more attractive.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |