High Integrity Floating Point Computation

Responsible KEG Investigator:
Dr Michal Konečný

Project Collaborator(s):

  • Praxis High Integrity Systems, Ltd
Type of Project: Case Award

Funder: EPSRC

Date Commissioned: 10/2005
Date Completed: 03/2009

Project Summary
The project's aim is to add the ability to verify floating point programs to the SPARK/SPADE language and tools.