Skip to main content
SpringerLink
Log in

Hardware-Dependent Proofs of Numerical Programs

  • Conference paper
Certified Programs and Proofs (CPP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7086))

Included in the following conference series:

Abstract

We present an approach for proving behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers.

The approach is implemented on top of the generic Why platform for deductive verification, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.

This work was partly funded by the U3CAT project (ANR-08-SEGI-021, http://frama-c.com/u3cat/ ) of the French national research organization (ANR), and the Hisseo project, funded by Digiteo ( http://hisseo.saclay.inria.fr/ )

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. IEEE standard for floating-point arithmetic. Technical report (2008), http://dx.doi.org/10.1109/IEEESTD.2008.4610935

  2. Ayad, A., Marché, C.: Multi-Prover Verification of Floating-Point Programs. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 127–141. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: 6th PASTE, New York, NY, USA, pp. 82–87. ACM (2005)

    Google Scholar 

  4. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Barthe, G., Rezk, T., Saabas, A.: Proof Obligations Preserving Compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 112–126. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

  8. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  9. Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008), http://alt-ergo.lri.fr/

  10. Boldo, S., Filliâtre, J.-C.: Formal Verification of Floating-Point Programs. In: 18th ARITH, pp. 187–194 (June 2007)

    Google Scholar 

  11. Boldo, S., Marché, C.: Formal verification of numerical programs: from C annotated programs to mechanical proofs. In: Mathematics in Computer Science (2011)

    Google Scholar 

  12. Boldo, S., Nguyen, T.M.T.: Hardware-independent proofs of numerical programs. In: 2nd NASA Formal Methods Symposium, pp. 14–23 (April 2010)

    Google Scholar 

  13. Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering 7, 151–160 (2011)

    Article  Google Scholar 

  14. Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166–192 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  15. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Technical Report NIII-R0309, Dept. of Computer Science, University of Nijmegen (2003)

    Google Scholar 

  16. Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: SAC, pp. 1835–1839. ACM (2006)

    Google Scholar 

  17. Carreño, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: HOL 1995 (September 1995)

    Google Scholar 

  18. Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: PLDI, pp. 95–107. ACM (2000)

    Google Scholar 

  19. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Cuoq, P., Prevosto, V.: Value Plugin Documentation, Carbon version. In: CEA-List (2011), http://frama-c.com/download/frama-c-value-analysis.pdf

  21. de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an Industrial use of FLUCTUAT on Safety-Critical Avionics Software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Dowek, G., Muñoz, C.: Conflict detection and resolution for 1,2,.,N aircraft. In: 7th AIAA Aviation, Technology, Integration, and Operations Conference (2007)

    Google Scholar 

  24. Filliâtre, J.-C.: Formal Verification of MIX Programs. In: Journées en l’honneur de Donald E. Knuth (2007), http://knuth07.labri.fr/exposes.php

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

  26. Harrison, J.: 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 

  27. Leavens, G.T.: Not a number of floating point problems. Journal of Object Technology 5(2), 75–83 (2006)

    Article  Google Scholar 

  28. Melquiond, G.: Proving Bounds on Real-Valued Functions with Computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 2–17. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Monniaux, D.: The pitfalls of verifying floating-point computations. Transactions on Programming Languages and Systems 30(3), 12 (2008)

    Article  Google Scholar 

  30. Moy, Y., Marché, C.: Jessie Plugin Tutorial, Beryllium version. INRIA (2009), http://www.frama-c.cea.fr/jessie.html

  31. Myreen, M.O.: Formal verification of machine-code programs. PhD thesis, University of Cambridge (2008)

    Google Scholar 

  32. Nguyen, T.M.T., Marché, C.: Proving floating-point numerical programs by analysis of their assembly code. Research Report 7655, INRIA (2011), http://hal.inria.fr/inria-00602266/en/

  33. Rival, X.: Abstract Interpretation-Based Certification of Assembly Code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 41–55. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  34. 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 Journal of Computation and Mathematics 1, 148–200 (1998)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Thi Minh Tuyen Nguyen & Claude Marché

  2. Lab. de Recherche en Informatique, Univ Paris-Sud, CNRS, Orsay, F-91405, France

    Thi Minh Tuyen Nguyen & Claude Marché

Authors
  1. Thi Minh Tuyen Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claude Marché
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Tsinghua University, FIT 3-603, 100084, Beijing, China

    Jean-Pierre Jouannaud

  2. Department of Computer Science, Yale University, 51 Prospect Street, 06520-8285, New Haven, CT, USA

    Zhong Shao

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nguyen, T.M.T., Marché, C. (2011). Hardware-Dependent Proofs of Numerical Programs. In: Jouannaud, JP., Shao, Z. (eds) Certified Programs and Proofs. CPP 2011. Lecture Notes in Computer Science, vol 7086. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25379-9_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25379-9_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25378-2

  • Online ISBN: 978-3-642-25379-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation