Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 10381))
Included in the following conference series:
460Accesses
Abstract
We present a fullCoq formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers, using computation intensive proofs and a continued fractions library built for this formalisation.
This work was partially funded by the ANR projectFastRelax (ANR-14-CE25-0018-01) of the French National Agency for Research.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Note that this was proved to match the original paper, but all results could have been proven the same way by just using 225799 everywhere instead of\(\lceil 2^{19} \cdot \log _5 2\rfloor \).
References
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci.9(1), 41–62 (2015)
Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) 20th IEEE Symposium on Computer Arithmetic, ARITH 2011, Tübingen, Germany, 25–27 July 2011, pp. 243–252. IEEE Computer Society (2011)
Brisebarre, N., Lauter, C.Q., Mezzarobba, M., Muller, J.: Comparison between binary and decimal floating-point numbers. IEEE Trans. Comput.65(7), 2032–2044 (2016)
Brisebarre, N., Mezzarobba, M., Muller, J., Lauter, C.Q.: Comparison between binary64 and decimal64 floating-point numbers. In: Nannarelli, A., Seidel, P., Tang, P.T.P. (eds.) 21st IEEE Symposium on Computer Arithmetic, ARITH 2013, Austin, TX, USA, April 7–10 2013, pp. 145–152. IEEE Computer Society (2013)
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_8
Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. Technical report RR-6455, INRIA (2008)
Khinchin, A., Eagle, H.: Continued Fractions. Dover Books on Mathematics. Dover Publications, Mineola (1964)
Martin-Dorel, É., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason.57(3), 187–217 (2016)
The Coq Development Team: The Coq Proof Assistant Reference Manual – Version V8.6, December 2016.http://coq.inria.fr
Author information
Authors and Affiliations
École Normale Supérieure de Lyon, Lyon, France
Arthur Blot & Jean-Michel Muller
Inria Sophia Antipolis - Université Côte d’Azur, Sophia Antipolis, France
Laurent Théry
- Arthur Blot
You can also search for this author inPubMed Google Scholar
- Jean-Michel Muller
You can also search for this author inPubMed Google Scholar
- Laurent Théry
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toArthur Blot.
Editor information
Editors and Affiliations
University of Oxford , Oxford, United Kingdom
Alessandro Abate
Université Paris-Sud, Inria , Orsay, France
Sylvie Boldo
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Blot, A., Muller, JM., Théry, L. (2017). Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. In: Abate, A., Boldo, S. (eds) Numerical Software Verification. NSV 2017. Lecture Notes in Computer Science(), vol 10381. Springer, Cham. https://doi.org/10.1007/978-3-319-63501-9_3
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-319-63500-2
Online ISBN:978-3-319-63501-9
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative