Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. (English) Zbl 1427.65064
Bjørner, Nikolaj (ed.) et al., FM 2015: formal methods. 20th international symposium, Oslo, Norway, June 24–26, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9109, 532-550 (2015).
Summary: Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide overestimates. Also, there are no available rigorous approaches that handle transcendental functions. We have developed a new approach called Symbolic Taylor Expansions that avoids this difficulty, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. In addition to providing far tighter upper bounds of round-off error in a vast majority of cases, FPTaylor also emits analysis certificates in the form of HOL Light proofs. We release FPTaylor along with our benchmarks for evaluation.
For the entire collection see [Zbl 1350.68006].
For the entire collection see [Zbl 1350.68006].
References:
| [1] | Alliot, J.M., Durand, N., Gianazza, D., Gotteland, J.B.: Implementing an interval computation library for OCaml on x86/amd64 architectures (short paper). In: ICFP 2012. ACM (2012) |
| [2] | Barr, E. T.; Vo, T.; Le, V.; Su, Z., Automatic Detection of Floating-point Exceptions, POPL 2013, 549-560 (2013), New York: ACM, New York · Zbl 1301.68087 |
| [3] | Bingham, J.; Leslie-Hurd, J.; Biere, A.; Bloem, R., Verifying Relative Error Bounds Using Symbolic Simulation, Computer Aided Verification, 277-292 (2014), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-319-08867-9_18 |
| [4] | Boldo, S.; Clément, F.; Filliâtre, J. C.; Mayero, M.; Melquiond, G.; Weis, P., Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, 50, 4, 423-456 (2013) · Zbl 1267.68208 · doi:10.1007/s10817-012-9255-4 |
| [5] | Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: FMCAD 2009, pp. 69-76 (2009) |
| [6] | Chen, L.; Miné, A.; Cousot, P.; Ramalingam, G., A Sound Floating-Point Polyhedra Abstract Domain, Programming Languages and Systems, 3-18 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-89330-1_2 |
| [7] | Chiang, W. F.; Gopalakrishnan, G.; Rakamarić, Z.; Solovyev, A., Efficient Search for Inputs Causing High Floating-point Errors, PPoPP 2014, 43-52 (2014), New York: ACM, New York |
| [8] | Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93-107. Springer, Heidelberg (2013) · Zbl 1381.68153 |
| [9] | The Coq Proof Assistant, http://coq.inria.fr/ · Zbl 1465.03051 |
| [10] | Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X.; Sagiv, M., The ASTREÉ Analyzer, Programming Languages and Systems, 21-30 (2005), Heidelberg: Springer, Heidelberg · Zbl 1108.68422 · doi:10.1007/978-3-540-31987-0_3 |
| [11] | Cousot, P.; Cousot, R., Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, POPL 1977, 238-252 (1977), New York: ACM, New York |
| [12] | Daramy, C.; Defour, D.; de Dinechin, F.; Muller, J. M., CR-LIBM: a correctly rounded elementary function library, Proc. SPIE, 5205, 458-464 (2003) |
| [13] | Darulova, E.; Kuncak, V., Trustworthy Numerical Computation in Scala, OOPSLA 2011, 325-344 (2011), New York: ACM, New York |
| [14] | Darulova, E.; Kuncak, V., Sound Compilation of Reals, POPL 2014, 235-248 (2014), New York: ACM, New York · Zbl 1284.68393 |
| [15] | Daumas, M., Melquiond, G.: Certification of Bounds on Expressions Involving Rounded Operators. ACM Trans. Math. Softw. 37(1), 2:1-2:20 (2010) · Zbl 1364.68328 |
| [16] | Delmas, D.; Goubault, E.; Putot, S.; Souyris, J.; Tekkal, K.; Védrine, F.; Alpuente, M.; Cook, B.; Joubert, C., Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, Formal Methods for Industrial Critical Systems, 53-69 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-04570-7_6 |
| [17] | 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) · Zbl 1365.65302 |
| [18] | Frama-C Software Analyzers, http://frama-c.com/ |
| [19] | Gáti, A.: Miller Analyzer for Matlab: A Matlab Package for Automatic Roundoff Analysis. Computing and Informatics 31(4), 713- (2012) · Zbl 1399.65115 |
| [20] | Giannakopoulou, D.; Howar, F.; Isberner, M.; Lauderdale, T.; Rakamarić, Z.; Raman, V., Taming Test Inputs for Separation Assurance, ASE 2014, 373-384 (2014), New York: ACM, New York |
| [21] | Goodloe, A. E.; Muñoz, C.; Kirchner, F.; Correnson, L.; Brat, G.; Rungta, N.; Venet, A., Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, NASA Formal Methods, 441-446 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-38088-4_31 |
| [22] | Goualard, F.: How Do You Compute the Midpoint of an Interval? ACM Trans. Math. Softw., 40(2) 11:1-11:25 (2014) · Zbl 1305.65252 |
| [23] | Goubault, E.; Putot, S.; Jhala, R.; Schmidt, D., Static Analysis of Finite Precision Computations, Verification, Model Checking, and Abstract Interpretation, 232-247 (2011), Heidelberg: Springer, Heidelberg · Zbl 1317.68116 · doi:10.1007/978-3-642-18275-4_17 |
| [24] | Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: FMCAD 2012, pp. 131-140 (2012) · Zbl 1317.68110 |
| [25] | Harrison, J. V.; Hunt, W. A. Jr.; Johnson, S. D., Formal Verification of Floating Point Trigonometric Functions, Formal Methods in Computer-Aided Design, 217-233 (2000), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-40922-X_14 |
| [26] | Harrison, J.; Bernardo, M.; Cimatti, A., Floating-Point Verification Using Theorem Proving, Formal Methods for Hardware Verification, 211-242 (2006), Heidelberg: Springer, Heidelberg · Zbl 1182.68120 · doi:10.1007/11757283_8 |
| [27] | Harrison, J.; Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., HOL Light: An Overview, Theorem Proving in Higher Order Logics, 60-66 (2009), Heidelberg: Springer, Heidelberg · Zbl 1252.68255 · doi:10.1007/978-3-642-03359-9_4 |
| [28] | IEEE Standard for Floating-point Arithmetic. IEEE Std 754-2008, pp. 1-70 (2008) |
| [29] | Johnson, S.G.: The NLopt nonlinear-optimization package, http://ab-initio.mit.edu/nlopt |
| [30] | Kearfott, R. B., GlobSol User Guide, Optimization Methods Software, 24, 4-5, 687-708 (2009) · Zbl 1180.90314 · doi:10.1080/10556780802614051 |
| [31] | Lebbah, Y., ICOS: A Branch and Bound Based Solver for Rigorous Global Optimization, Optimization Methods Software, 24, 4-5, 709-726 (2009) · Zbl 1179.90265 · doi:10.1080/10556780902753452 |
| [32] | Leeser, M., Mukherjee, S., Ramachandran, J., Wahl, T.: Make it real: Effective floating-point reasoning via exact arithmetic. In: DATE 2014, pp. 1-4 (2014) |
| [33] | Linderman, M. D.; Ho, M.; Dill, D. L.; Meng, T. H.; Nolan, G. P., Towards Program Optimization Through Automated Analysis of Numerical Precision, CGO 2010, 230-237 (2010), New York: ACM, New York |
| [34] | Martel, M., Semantics of roundoff error propagation in finite precision calculations, Higher-Order and Symbolic Computation, 19, 1, 7-30 (2006) · Zbl 1105.65052 · doi:10.1007/s10990-006-8608-2 |
| [35] | Martel, M., Program Transformation for Numerical Precision, PEPM 2009, 101-110 (2009), New York: ACM, New York |
| [36] | Martel, M., RangeLab: A Static-Analyzer to Bound the Accuracy of Finite-Precision Computations, SYNASC 2011, 118-122 (2011), Washington, DC: IEEE Computer Society, Washington, DC |
| [37] | Maxima: Maxima, a Computer Algebra System. Version 5.30.0 (2013), http://maxima.sourceforge.net/ |
| [38] | Melquiond, G., Floating-point arithmetic in the Coq system, Information and Computation, 216, 14-23 (2012) · Zbl 1257.68131 · doi:10.1016/j.ic.2011.09.005 |
| [39] | Mikusinski, P., Taylor, M.: An Introduction to Multivariable Analysis from Vector to Manifold. Birkhäuser Boston (2002) · Zbl 0997.26001 |
| [40] | Miller, W., Software for Roundoff Analysis, ACM Trans. Math. Softw., 1, 2, 108-128 (1975) · Zbl 0303.65036 · doi:10.1145/355637.355639 |
| [41] | Moore, R.: Interval analysis. Prentice-Hall series in automatic computation, Prentice-Hall (1966) · Zbl 0176.13301 |
| [42] | de Moura, L.; Bjørner, N. S.; Ramakrishnan, C. R.; Rehof, J., Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [43] | Mutrie, M. P.W.; Bartels, R. H.; Char, B. W., An Approach for Floating-point Error Analysis Using Computer Algebra, ISSAC 1992, 284-293 (1992), New York: ACM, New York · Zbl 0919.65033 |
| [44] | Neumaier, A., Taylor Forms - Use and Limits, Reliable Computing, 2003, 9-43 (2002) · Zbl 1071.65070 |
| [45] | Neumaier, A., Complete search in continuous global optimization and constraint satisfaction, Acta Numerica, 13, 271-369 (2004) · Zbl 1113.90124 · doi:10.1017/S0962492904000194 |
| [46] | OpenOpt: universal numerical optimization package, http://openopt.org |
| [47] | Paganelli, G., Ahrendt, W.: Verifying (In-)Stability in Floating-Point Programs by Increasing Precision, Using SMT Solving. In: SYNASC, 2013, pp. 209-216 (2013) |
| [48] | Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically Improving Accuracy for Floating Point Expressions. In: PLDI 2015. ACM (2015) |
| [49] | Ponsini, O., Michel, C., Rueher, M.: Verifying floating-point programs with constraint programming and abstract interpretation techniques. Automated Software Engineering, 1-27 (2014) |
| [50] | Rakamarić, Z.; Emmi, M.; Biere, A.; Bloem, R., SMACK: Decoupling Source Language Details from Verifier Implementations, Computer Aided Verification, 106-113 (2014), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-319-08867-9_7 |
| [51] | Revol, N.; Makino, K.; Berz, M., Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY, The Journal of Logic and Algebraic Programming, 64, 1, 135-154 (2005) · Zbl 1080.68519 · doi:10.1016/j.jlap.2004.07.008 |
| [52] | Rümmer, P., Wahl, T.: An SMT-LIB Theory of Binary Floating-Point Arithmetic. In: SMT Workshop 2010 (2010) |
| [53] | Solovyev, A.; Hales, T. C.; Brat, G.; Rungta, N.; Venet, A., Formal verification of nonlinear inequalities with taylor interval approximations, NASA Formal Methods, 383-397 (2013), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-38088-4_26 |
| [54] | Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. Tech. Rep. UUCS-15-001, School of Computing, University of Utah (2015) · Zbl 1427.65064 |
| [55] | Stolfi, J.; de Figueiredo, L., An Introduction to Affine Arithmetic, TEMA Tend. Mat. Apl. Comput., 4, 3, 297-312 (2003) · Zbl 1208.65057 |
| [56] | Stoutemyer, D. R., Automatic Error Analysis Using Computer Algebraic Manipulation, ACM Trans. Math. Softw., 3, 1, 26-43 (1977) · Zbl 0348.65037 · doi:10.1145/355719.355721 |
| [57] | NASA World Wind Java SDK, http://worldwind.arc.nasa.gov/java/ |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
