- Carreno, Victor A; and Miner, Paul S. :
*Specification of the IEEE-854 Floating-Point Standard in HOL and PVS*. Presented at the 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications, September 11-14, 1995, Aspen Grove, Utah as a track B paper and included in supplemental proceedings**Abstract**: The IEEE-854 Standard for radix-independent floating-point arithmetic has been partially defined within two mechanical verification systems. We present the specification of key parts of the standard in both HOL and PVS. This effort to formalize IEEE-854 has given the opportunity to compare the styles imposed by the two verification systems on the specification. - Carreno, Victor A.:
*Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System*, NASA Technical Memorandum 110189, September 1995.**Abstract**: The ANSI/IEEE Standard 854-1987 for floating-point arithmetic is interpreted by converting the lexical descriptions in the standard into mathematical conditional descriptions organized in tables. The standard is represented in higher-order logic within the framework of the HOL system. The paper is divided in two parts with the first part the interpretation and the second part the description in HOL. - Miner, Paul S.:
*Defining the IEEE-854 Floating-Point Standard in PVS*, NASA Technical Memorandum 110167, June 1995.**Abstract**: A significant portion of the ANSI/IEEE-854 Standard for Radix-Independent Floating-Point Arithmetic is defined in PVS (Prototype Verification System). Since IEEE-854 is a generalization of the ANSI/IEEE-754 Standard for Binary Floating-Point Arithmetic, the definition of IEEE-854 in PVS also formally defines much of IEEE-754. This collection of PVS theories provides a basis for machine checked verification of floating-point systems. This formal definition illustrates that formal specification techniques are sufficiently advanced that it is reasonable to consider their use in the development of future standards.The PVS theories are available via FTP.

Curator and Responsible NASA Official: C. Michael Holloway

last modified: 23 September 1998 (11:47:15)