[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Geof Barrett
- Formal Methods Applied to a Floating Point Number System
- Technical Monograph 58 PRG Oxford 1987
- =EXPERIENCE PROOF Floating-point operations STANDARD
used Hoare/Floyd-style proofs to prove that Inmos' software
floating-point package satisfied its specification, a Z-ified version of
the IEEE-754 standard. This software fp package was the starting point for the formally-derived microcode for the FPU in the Inmos T800 transputer. This was certainly a real-world application; moreover, the formal approach overtook the informal approach, and in the process they found an inconsistency and an ambiguity in the IEEE standard, and a bug in a competitor's chip. Inmos and the PRG (Oxford) were awarded a Queen's Award for Technological Achievement for the T800 project.
Includes Floating point IEEE TSE paper -- where is it?
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]