Advertisement

Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions

  • Joachim Bard
  • Heiko BeckerEmail author
  • Eva Darulova
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

When compared to idealized, real-valued arithmetic, finite precision arithmetic introduces unavoidable errors, for which numerous tools compute sound upper bounds. To ensure soundness, providing formal guarantees on these complex tools is highly valuable.

In this paper we extend one such formally verified tool, FloVer. First, we extend FloVer with an SMT-based domain using results from an external SMT solver as an oracle. Second, we implement interval subdivision on top of the existing analyses. Our evaluation shows that these extensions allow FloVer to efficiently certify more precise bounds for nonlinear expressions.

Keywords

Coq Roundoff error Finite-precision SMT Subdivision 

References

  1. 1.
    The Coq Proof Assistant. https://coq.inria.fr
  2. 2.
    The HOL4 Theorem Prover. https://hol-theorem-prover.org/
  3. 3.
    Becker, H., Zyuzin, N., Monat, R., Darulova, E., Myreen, M.O., Fox, A.: A verified certificate checker for finite-precision error bounds in Coq and HOL4. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–10. IEEE (2018)Google Scholar
  4. 4.
    Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy - framework for analysis and optimization of numerical programs (tool paper). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 270–287. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_15CrossRefGoogle Scholar
  5. 5.
    Darulova, E., Kuncak, V.: Towards a compiler for reals. ACM Trans. Prog. Lang. Syst. (TOPLAS) 39(2), 8 (2017)Google Scholar
  6. 6.
    De Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: ACM Symposium on Applied Computing (SAC) (2006)Google Scholar
  7. 7.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  8. 8.
    de Figueiredo, L.H., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1–4), 147–158 (2004)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_17CrossRefGoogle Scholar
  10. 10.
    Magron, V., Constantinides, G., Donaldson, A.: Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw. (TOMS) 43(4), 34 (2017)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Moore, R.: Interval Analysis. Prentice-Hall, New Jersey (1966)zbMATHGoogle Scholar
  12. 12.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55602-8_217CrossRefGoogle Scholar
  13. 13.
    Solovyev, A., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. In: International Symposium on Formal Methods (FM) (2015)Google Scholar
  14. 14.
    Titolo, L., Feliú, M.A., Moscato, M., Muñoz, C.A.: An abstract interpretation framework for the round-off error analysis of floating-point programs. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 516–537. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-73721-8_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.MPI-SWS, Saarland Informatics CampusSaarbrückenGermany

Personalised recommendations