Loading...
Please wait, while we are loading the content...
Similar Documents
Specification of the IEEE-854 Floating-Point Standard in HOL and PVS (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Miner, Paul S. Carreño, Victor A. |
| 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. 1 Introduction The HOL [3] and PVS [7] systems are general purpose mechanical verification systems whose specification languages are based on higher-order logic. We have partially defined the ANSI/IEEE-854 standard for radix-independent floating-point arithmetic [5] in both of these verification systems [2, 6]. This effort to formalize IEEE-854 has given the opportunity to compare the styles imposed by the two verification systems on the specification. This is not the first formalization of floating-point arithmetic. Geoff Barrett [1] describes the Z formalization of IEEE-754 used in the development of the INMOS T800 Transputer... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Ansi Ieee-854 Standard Radix-independent Floating-point Arithmetic Inmos T800 Transputer General Purpose Mechanical Verification System Geoff Barrett First Formalization Ieee-854 Standard Ieee-854 Floating-point Standard Verification System Mechanical Verification System |
| Content Type | Text |
