Skip to main content
Conference Proceedings

Floating point verification in HOL

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1995) 971 186-199
DOI: 10.1007/3-540-60275-5_65
14Citations
Citations of this article
12Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Floating-point verification is a very interesting application area for theorem provers. HOL is a general-purpose prover which is equipped with an extensive and rigorous theory of real analysis. We explain how it can be used in floating point verification, illustrating our remarks with complete verifications of simple square-root and (natural) logarithm algorithms.

Cite

CITATION STYLE

APA

Harrison, J. (1995). Floating point verification in HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 971, pp. 186–199). Springer Verlag. https://doi.org/10.1007/3-540-60275-5_65

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free