| EPSRC Reference: |
GR/K58395/01 |
| Title: |
FLOATING - POINT VERIFICATION |
| 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 September 1996 |
Ends: |
29 February 2000 |
Value (£): |
181,605
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The goal is to demonstrate that it is practical, using existing theorem proving technology, to formally verify industrially signficant floating point algorithms and their implementations.Models of such algorithms will be mechanically verified with the HOL theorem proving system against precise specifications, often based on real numbers. Industry is sceptical about the value of formal verification. It is hoped that our studies will help convince manufacturers that the potential benefits far outweigh the costs. This could have tremendous impact on the industrial uptake of 'formal methods'.
|
|
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 |