Marc Daumas
Guillaume Melquiond
Abstract
Gappa is a tool designed to formally verify the correctness of numerical software and hardware. It uses interval arithmetic and forward error analysis to bound mathematical expressions that involve rounded as well as exact operators. It then generates a theorem and its proof for each verified enclosure. This proof can be automatically checked with a proof assistant, such as Coq or HOL Light. It relies on a large companion library of facts that we have developed. This Coq library provides theorems dealing with addition, multiplication, division, and square root, for both fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature can be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is suited to discharge proof obligations generated for small pieces of software. They may be produced by third-party tools and the first applications of Gappa use proof obligations written by designers or obtained from traces of execution.
- Boldo, S. and Daumas, M. 2004. A simple test qualifying the accuracy of Horner's rule for polynomials. Numer. Alg. 37, 1-4, 45--60.Google Scholar
Cross Ref
- Boldo, S., Daumas, M., and Giorgi, P. 2008. Formal proof for delayed finite field arithmetic using floating point operators. In Proceedings of the Conference on Real Numbers and Computers (Santiago de Compostela, Spain).Google Scholar
- Boldo, S. and Filliâtre, J.-C. 2007. Formal verification of floating point programs. In Proceedings of the 18th Symposium on Computer Arithmetic (Montpellier, France). Google ScholarDigital Library
- Boldo, S. and Melquiond, G. 2008. Emulation of a FMA and correctly rounded sums: proved algorithms using rounding to odd. IEEE Trans. Comput. 57, 4, 462--471. Google ScholarDigital Library
- Boutin, S. 1997. Using reflection to build efficient and certified decision procedures. In Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software (London, U.K.). 515--529. Google ScholarDigital Library
- Brönnimann, H., Melquiond, G., and Pion, S. 2006. The design of the Boost interval arithmetic library. Theor. Comput. Sci. 351, 111--118. Google ScholarDigital Library
- Daumas, M., Lester, D., and Muoz, C. 2009. Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput. 58, 2, 226--237. Google ScholarDigital Library
- Daumas, M. and Melquiond, G. 2004. Generating formally certified bounds on values and round-off errors. In Proceedings of the Conference on Real Numbers and Computers (Dagstuhl, Germany). 55--70.Google Scholar
- Daumas, M., Melquiond, G., and Muñoz, C. 2005. Guaranteed proofs using interval arithmetic. In Proceedings of the 17th Symposium on Computer Arithmetic (Cape Code, MA), P. Montuschi and E. Schwarz, Eds. 188--195. Google ScholarDigital Library
- de Dinechin, F., Defour, D., and Lauter, C. 2004. Fast correct rounding of elementary functions in double precision using double-extended arithmetic. Research rep. 5137. Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France.Google Scholar
- de Dinechin, F., Lauter, C. Q., and Melquiond, G. 2006. Assisted verification of elementary functions using Gappa. In Proceedings of the ACM Symposium on Applied Computing (Dijon, France). 1318--1322. Google ScholarDigital Library
- Even, G. and Seidel, P.-M. 1999. A comparison of three rounding algorithms for IEEE floating-point multiplication. In Proceedings of the 14th Symposium on Computer Arithmetic (Adelaide, Australia), I. Koren and P. Kornerup, Eds. 225--232. Google ScholarDigital Library
- Filliâtre, J.-C. 2003. Why: A multi-language multi-prover verification tool. Research rep. 1366, Université Paris Sud.Google Scholar
- Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., and Zimmermann, P. 2005. MPFR: A multiple-precision binary floating-point library with correct rounding. Tech. rep. RR-5753. INRIA, Rocquencourt, France.Google Scholar
- Gameiro, M. and Manolios, P. 2004. Formally verifying an algorithm based on interval arithmetic for checking transversality. In Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications (Austin, TX). 17.Google Scholar
- Harrison, J. 1997. Floating point verification in HOL light: The exponential function. Technical rep. 428. University of Cambridge Computer Laboratory, Cambridge, U.K.Google Scholar
- Harrison, J. 2000. The HOL Light Manual. Version 1.1.Google Scholar
- Higham, N. J. 2002. Accuracy and Stability of Numerical Algorithms, SIAM, 2nd ed. Philadelphia, PA. Google ScholarDigital Library
- Huet, G., Kahn, G., and Paulin-Mohring, C. 2004. The Coq proof assistant: A tutorial, version 8.0 Tech. rep. INRIA, Rocquencourt, France.Google Scholar
- Jaulin, L., Kieffer, M., Didrit, O., and Walter, E. 2001. Applied Interval Analysis. Springer, Berlin, Germany.Google Scholar
- Kahan, W. 1965. Further remarks on reducing truncation errors. Commun. ACM 8, 1, 40. Google ScholarDigital Library
- Kaufmann, M., Manolios, P., and Moore, J. S. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht, The Netherlands. Google ScholarDigital Library
- Melquiond, G. and Pion, S. 2007. Formally certified floating-point filters for homogeneous geometric predicates. Theoret. Informat. Appl. 41, 1, 57--70.Google ScholarCross Ref
- Michard, R., Tisserand, A., and Veyrat-Charvillon, N. 2006. Optimisation d'opêrateurs arithmétiques matériels base d' approximations polynomiales. In Proceedings of the Symposium en Architecture de Machines (Perpignan, France). 1318--1322.Google Scholar
- Neumaier, A. 1990. Interval Methods for Systems of Equations. Cambridge University Press, Cambridge, U.K.Google Scholar
- Owre, S., Rushby, J. M., and Shankar, N. 1992. PVS: A prototype verification system. In 11th International Conference on Automated Deduction, D. Kapur, Ed. Springer-Verlag, New York, NY. 748--752. Google ScholarDigital Library
- Putot, S., Goubault, E., and Martel, M. 2004. Static analysis based validation of floating point computations. In Novel Approaches to Verification. Lecture Notes in Computer Science, vol. 2991. Springer, Dagstuhl, Germany, 306--313.Google Scholar
- Revy, G. 2006. Analyse et implantation d'algorithmes rapides pour l'évaluation polynomiale sur les nombres flottants. Tech. rep. ensl-00119498. École Normale Supérieure de Lyon, Lyon, France.Google Scholar
- Rockwell Collins. 2005. Rockwell Collins receives MILS certification from NSA on microprocessor. Press releases. www.rockwellcolling.com.Google Scholar
- Rump, S. M., Ogita, T., and Oishi, S. 2005. Accurate floating-point summation. Tech. rep. 05.12. Hamburg University of Technology, Hamburg, Germany.Google Scholar
- Schlumberger. 2003. Schlumberger leads the way in smart card security with common criteria EAL7 security methodology. Press releases. www.slb.com.Google Scholar
- Stevenson, D. et al. 1987. An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Not. 22, 2, 9--25.Google Scholar
- Tang, P. T. P. 1989. Table driven implementation of the exponential function in IEEE floating point arithmetic. ACM Trans. Math. Softw. 15, 2, 144--157. Google ScholarDigital Library
- Tiwari, A., Shankar, N., and Rushby, J. 2003. Invisible formal methods for embedded control systems. Proc. IEEE 91, 1, 29--39.Google ScholarCross Ref
Index Terms
- Certification of bounds on expressions involving rounded operators
Recommendations
Proof-checking Euclid
We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used ...
Experiences from Exporting Major Proof Assistant Libraries
AbstractThe interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Comments