caa a22 4500 475797493 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000601xx s 000 0 eng 10.1023/A:1008712907154 doi (NATIONALLICENCE)springer-10.1023/A:1008712907154 Harrison John University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, CB2 3QG, Cambridge, England aut Floating Point Verification in HOL Light: The Exponential Function [Elektronische Daten] [John Harrison] Since they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previousl published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally. The development described here includes, apart from the proof itself, a formalization of IEEE arithmetic, a mathematical semantics for the programming language in which the algorithm is expressed, and the body of pure mathematics needed. All this is developed logically from first principles using the HOL Light prover, which guarantees strict adherence to simple rules of inference while allowing the user to perform proofs using higher-level derived rules. Kluwer Academic Publishers, 2000 Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 271-305 0925-9856 16:3<271 2000 16 10703 https://doi.org/10.1023/A:1008712907154 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008712907154 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Harrison John University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, CB2 3QG, Cambridge, England aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 271-305 0925-9856 16:3<271 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer