[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Barrett87

  1. Geof Barrett
  2. Formal Methods Applied to a Floating Point Number System
  3. Technical Monograph 58 PRG Oxford 1987
  4. =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 uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]