Skip to main content
SpringerLink
Log in

Combining Coq and Gappa for Certifying Floating-Point Programs

  • Conference paper
Intelligent Computer Mathematics (CICM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5625))

Included in the following conference series:

Abstract

Formal verification of numerical programs is notoriously difficult. On the one hand, there exist automatic tools specialized in floating-point arithmetic, such as Gappa, but they target very restrictive logics. On the other hand, there are interactive theorem provers based on the LCF approach, such as Coq, that handle a general-purpose logic but that lack proof automation for floating-point properties. To alleviate these issues, we have implemented a mechanism for calling Gappa from a Coq interactive proof. This paper presents this combination and shows on several examples how this approach offers a significant speedup in the process of verifying floating-point programs.

This research was partially supported by projects ANR-05-BLAN-0281-04 “CerPAN” and ANR-08-BLAN-0246-01 “F\(\oint\)ST”.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Microprocessor Standards Subcommittee: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008, pp. 1–58 (August 2008)

    Google Scholar 

  2. O’Leary, J., Zhao, X., Gerth, R., Seger, C.J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal (Q1), 1–10 (February 1999)

    Google Scholar 

  3. Reeber, E., Sawada, J.: Combining ACL2 and an automated verification tool to verify a multiplier. In: Manolios, P., Wilding, M. (eds.) 6th International Workshop on the ACL2 Theorem Prover and its Applications, August 2006, pp. 63–70 (2006)

    Google Scholar 

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

    Google Scholar 

  5. Harrison, J.: A machine-checked theory of floating-point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): Semantical Combination of Congruence Closure with Solvable Theories. In: 5th International Workshop on Satisfiability Modulo Theories (SMT 2007). Electronic Notes in Computer Science, vol. 198(2), pp. 51–69. Elsevier Science Publishers, Amsterdam (1985)

    Google Scholar 

  9. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580, 583 (1969)

    Article  MATH  Google Scholar 

  10. Boldo, S., Filliâtre, J.C.: Formal Verification of Floating-Point Programs. In: 18th IEEE International Symposium on Computer Arithmetic, Montpellier, France, June 2007, pp. 187–194 (2007)

    Google Scholar 

  11. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  12. The Coq Development Team: The Coq Proof Assistant Reference Manual – Version V8.2. (2008), http://coq.inria.fr/

  13. Mayero, M.: The Three Gap Theorem (Steinhauss conjecture). In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 162–173. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. Daumas, M., Rideau, L., Théry, L.: A generic library of floating-point numbers and its application to exact computing. In: 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 169–184 (2001)

    Google Scholar 

  15. Boldo, S.: Preuves formelles en arithmétiques à virgule flottante. PhD thesis, École Normale Supérieure de Lyon (November 2004)

    Google Scholar 

  16. Boldo, S.: Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. In: 3rd International Joint Conference on Automated Reasoning (IJCAR), Seattle, USA, August 2006, pp. 52–66 (2006)

    Google Scholar 

  17. Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 2–17. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. de Dinechin, F., Lauter, C., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: ACM Symposium on Applied Computing, Dijon, France, pp. 1318–1322 (2006)

    Google Scholar 

  19. Melquiond, G.: De l’arithmétique d’intervalles à la certification de programmes. PhD thesis, École Normale Supérieure de Lyon, Lyon, France (November 2006)

    Google Scholar 

  20. Bécache, E.: Étude de schémas numériques pour la résolution de l’équation des ondes. ENSTA (September 2003)

    Google Scholar 

  21. Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming. LNCS. Springer, Heidelberg (2009)

    Google Scholar 

  22. Kahan, W.: On the Cost of Floating-Point Computation Without Extra-Precise Arithmetic (November 2004), http://www.cs.berkeley.edu/~wkahan/Qdrtcs.pdf

  23. Boldo, S., Daumas, M., Kahan, W., Melquiond, G.: Proof and certification for an accurate discriminant. In: 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg, Germany (September 2006)

    Google Scholar 

  24. Boldo, S.: Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers 58(2), 220–225 (2009)

    Article  MathSciNet  Google Scholar 

  25. Boutin, S.: Using reflection to build efficient and certified decision procedures. Theoretical Aspects of Computer Software, 515–529 (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Saclay - Île-de-France, ProVal, Orsay, F-91893

    Sylvie Boldo, Jean-Christophe Filliâtre & Guillaume Melquiond

  2. LRI, Université Paris-Sud, CNRS, Orsay, F-91405, France

    Sylvie Boldo, Jean-Christophe Filliâtre & Guillaume Melquiond

Authors
  1. Sylvie Boldo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Christophe Filliâtre
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Guillaume Melquiond
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada

    Jacques Carette

  2. Informatics, 2.02 Informatics Forum, University of Edinburgh, 10 Crichton street, EH8 9AB, Edinburgh, UK

    Lucas Dixon

  3. Department of Computer Science, University of Bologna, via Mura Anteo Zamboni, 7, 40127, Bologna, Italy

    Claudio Sacerdoti Coen

  4. Department of Computer Science MC 375, University of Western Ontario, N6A 5B7, London, ON, Canada

    Stephen M. Watt

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boldo, S., Filliâtre, JC., Melquiond, G. (2009). Combining Coq and Gappa for Certifying Floating-Point Programs. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds) Intelligent Computer Mathematics. CICM 2009. Lecture Notes in Computer Science(), vol 5625. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02614-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02614-0_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02613-3

  • Online ISBN: 978-3-642-02614-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation