Abstract
Intel is applying formal veri_cation to various pieces of mathematical software used in Merced, the _rst implementation of the new IA-64 architecture. This paper discusses the development of a generic floating point library giving de_nitions of the fundamental terms and containing formal proofs of important lemmas. We also briefly describe how this has been used in the veri_cation e_ort so far.
Cite
CITATION STYLE
Harrison, J. (1999). A machine-checked theory of floating point arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1690, pp. 113–130). Springer Verlag. https://doi.org/10.1007/3-540-48256-3_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
