Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Theory Exploration for Interactive Theorem Proving: Read chapter Read first chapter

2017 | Supplement | Chapter

Formal Verification of a Floating-Point Expansion Renormalization Algorithm

Authors : Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Many numerical problems require a higher computing precision than the one offered by standard floating-point formats. A common way of extending the precision is to use floating-point expansions. As the problems may be critical and as the algorithms used have very complex proofs (many sub-cases), a formal guarantee of correctness is a wish that can now be fulfilled, using interactive theorem proving. In this article we give a formal proof in Coq for one of the algorithms used as a basic brick when computing with floating-point expansions, the renormalization, which is usually applied after each operation. It is a critical step needed to ensure that the resulted expansion has the same property as the input one, and is more “compressed”. The formal proof uncovered several gaps in the pen-and-paper proof and gives the algorithm a very high level of guarantee.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics
next chapter How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
Literature
1.
Abad, A., Barrio, R., Dena, A.: Computing periodic orbits with arbitrary precision. Phys. Rev. E 84, 016701 (2011)CrossRef
2.
Bailey, D.H., Borwein, J.M.: High-precision arithmetic in mathematical physics. Mathematics 3(2), 337 (2015)CrossRef
3.
Boldo, S.: Iterators: where folds fail. In: Workshop on High-Consequence Control Verification, Toronto, Canada, July 2016
4.
Boldo, S., Daumas, M.: A mechanically validated technique for extending the available precision. In: 35th Asilomar Conference on Signals, Systems, and Computers, Pacific Grove, California, pp. 1299–1303 (2001)
5.
Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Tübingen, Germany, pp. 243–252, July 2011
6.
Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2) (2007). http://​www.​mpfr.​org/​
7.
Hida, Y., Li, X.S., Bailey, D.H.: Algorithms for quad-double precision floating-point arithmetic. In: Burgess, N., Ciminiera, L. (eds.) Proceedings of the 15th IEEE Symposium on Computer Arithmetic (ARITH 2016), Vail, CO, pp. 155–162, June 2001
8.
IEEE Computer Society: IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754-2008, August 2008
9.
Jeannerod, C.P., Rump, S.M.: Improved error bounds for inner products in floating-point arithmetic. SIAM J. Matrix Anal. Appl. 34(2), 338–344 (2013)MathSciNetCrossRef
10.
Joldes, M., Marty, O., Muller, J.M., Popescu, V.: Arithmetic algorithms for extended precision using floating-point expansions. IEEE Trans. Comput. PP(99), 1 (2015)MATH
11.
Joldes, M., Muller, J.-M., Popescu, V., Tucker, W.: CAMPARY: cuda multiple precision arithmetic library and applications. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 232–240. Springer, Cham (2016). doi:10.​1007/​978-3-319-42432-3_​29CrossRef
12.
Joldes, M., Popescu, V., Tucker, W.: Searching for sinks for the Hénon map using a multipleprecision GPU arithmetic library. SIGARCH Comput. Archit. News 42(4), 63–68 (2014)CrossRef
13.
Kornerup, P., Lefèvre, V., Louvet, N., Muller, J.M.: On the computation of correctly-rounded sums. In: Proceedings of the 19th IEEE Symposium on Computer Arithmetic (ARITH 2019), Portland, OR, June 2009
14.
Laskar, J., Gastineau, M.: Existence of collisional trajectories of mercury, mars and venus with the earth. Nature 459(7248), 817–819 (2009)CrossRef
15.
Muller, J.M., Brisebarre, N., de Dinechin, F., Jeannerod, C.P., Lefèvre, V., Melquiond, G., Revol, N., Stehlé, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkhäuser, Boston (2010)CrossRef
16.
17.
Priest, D.M.: Algorithms for arbitrary precision floating point arithmetic. In: Kornerup, P., Matula, D.W. (eds.) Proceedings of the 10th IEEE Symposium on Computer Arithmetic, pp. 132–144. IEEE Computer Society Press, Los Alamitos (1991)CrossRef
18.
Priest, D.M.: On properties of floating-point arithmetics: numerical stability and the cost of accurate computations. Ph.D. thesis, University of California at Berkeley (1992)
19.
Rump, S.M., Ogita, T., Oishi, S.: Accurate floating-point summation part I: faithful rounding. SIAM J. Sci. Comput. 31(1), 189–224 (2008)MathSciNetCrossRef
20.
Shewchuk, J.R.: Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discret. Comput. Geom. 18, 305–363 (1997)MathSciNetCrossRef
Metadata
Title
Formal Verification of a Floating-Point Expansion Renormalization Algorithm
Authors
Sylvie Boldo
Mioara Joldes
Jean-Michel Muller
Valentina Popescu
Copyright Year
2017
Publisher
Springer International Publishing
Book
Interactive Theorem Proving

Print ISBN: 978-3-319-66106-3

Electronic ISBN: 978-3-319-66107-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-66107-0_7

Premium Partner

    Image Credits