Skip to main content
SpringerLink
Log in

Formal Verification of Programs Computing the Floating-Point Average

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9407))

Included in the following conference series:

Abstract

The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.

This work was supported by both the VERASCO (ANR-11-INSE-003) and the FastRelax (ANR-14-CE25-0018-01) projects of the French National Agency for Research (ANR).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://www.ibiblio.org/pub/languages/fortran/ch4-9.html.

References

  1. Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, version 1.9 (2013). http://frama-c.cea.fr/acsl.html

  2. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages. Wrocław, Poland, August 2011

    Google Scholar 

  3. Boldo, S.: Deductive formal verification: how to make your floating-point programs behave. Thèse d’habilitation, Université Paris-Sud, October 2014

    Google Scholar 

  4. Boldo, S., Filliâtre, J.C.: Formal verification of floating-point programs. In: Kornerup, P., Muller, J.M. (eds.) Proceedings of the 18th IEEE Symposium on Computer Arithmetic, pp. 187–194. Montpellier, France, June 2007

    Google Scholar 

  5. Boldo, S., Marché, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. Math. Comput. Sci. 5, 377–393 (2011)

    Article  MATH  Google Scholar 

  6. Boldo, S., Melquiond, G.: Emulation of FMA and correctly-rounded sums: proved algorithms using rounding to odd. IEEE Trans. Comput. 57(4), 462–471 (2008)

    Article  MathSciNet  Google Scholar 

  7. 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, pp. 243–252. Tübingen, Germany (2011)

    Google Scholar 

  8. Carreño, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: HOL95: 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications. Aspen Grove, UT, September 1995

    Google Scholar 

  9. Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories : design and implementation. Logical Methods Comput. Sci. 8(3), 1–29 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  10. Daumas, M., Melquiond, G.: Certification of bounds on expressions involving rounded operators. Trans. Math. Softw. 37(1), 1–20 (2010)

    Article  MathSciNet  Google Scholar 

  11. Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv. 23(1), 5–48 (1991)

    Article  Google Scholar 

  12. Harrison, J.V.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr, W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 217–233. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. IEEE standard for binary floating-point arithmetic. ANSI/IEEE Std 754–1985 (1985)

    Google Scholar 

  14. IEEE standard for floating-point arithmetic. IEEE Std 754–2008, August 2008

    Google Scholar 

  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)

    Book  MATH  Google Scholar 

  16. Russinoff, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J. Comput. Math. 1, 148–200 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  17. Sterbenz, P.H.: Floating Point Computation. Prentice Hall, Englewood Cliffs (1974)

    Google Scholar 

Download references

Acknowledgments

The author is indebted to a referee of a previous version of this work, who rightfully pitied the fact that no program existed for a correctly-rounded average and pointed out the previously dismissed average2 function. The author is also thankful to P. Zimmermann and V. Lefèvre for constructive discussions that turned \(E_i+2 p+2\) into \(E_i+2 p+1\) in Theorem 2.

Author information

Authors and Affiliations

  1. LRI, Bâtiment 650, Inria, Université Paris-Sud, 91405, Orsay Cedex, France

    Sylvie Boldo

Authors
  1. Sylvie Boldo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvie Boldo .

Editor information

Editors and Affiliations

  1. Electronics and Computer Science, University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Université Paris-Sud, Orsay, France

    Sylvain Conchon

  3. Université Paris-Sud, Orsay, France

    Fatiha Zaïdi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Boldo, S. (2015). Formal Verification of Programs Computing the Floating-Point Average. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25423-4_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25422-7

  • Online ISBN: 978-3-319-25423-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation