EPSRC logo

Details of Grant 

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