Abstract
Formal verification of floating-point computations remains a challenge for the software engineer. Automated, specialized tools can handle floating-point computations well, but struggle with other types of data or memory reasoning. Specialized tools based on proof assistants are very powerful, but require a high degree of expertise. General-purpose tools for deductive verification of programs have added support for floating-point computations in recent years, but often the proved properties are limited to verifying ranges or absence of special values such as NaN or Infinity. Proofs of more complex properties, such as bounds on rounding errors, are generally reserved to experts and often require the use of either a proof assistant or a specialized solver as a backend.
In this article, we show how generic deductive verification tools based on general-purpose SMT solvers can be used to verify different kinds of properties on floating point computations up to bounds on rounding errors. The demonstration is done on a computation of a weighted average using floating-point numbers, using an approach which is heavily based on auto-active verification. We use the general-purpose tool SPARK for formal verification of Ada programs based on the SMT solvers Alt-Ergo, CVC4, and Z3 but it can in principle be carried out in other similar languages and tools such as Frama-C or KeY.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Ada uses the term subprogram to denote functions (which return a value) and procedures (which do not).
- 3.
It is the bound used for lemmas about division in the lemma library of SPARK (more about the lemma library later in this article).
- 4.
Lemma Lemma_Add_Is_Monotonic takes inputs between Float’First/2.0 and Float’Last/2.0 to statically ensure absence of overflows in the addition.
- 5.
- 6.
Note that we use \(10^{-7}\) as an approximation of Epsilon here. A more precise approximation could be considered, like \(6\times 10^{-8}\), but, from our experiments, it causes proofs of error bounds on basic operations to become out of reach of the automated SMT solvers used behind SPARK.
- 7.
Theoretically, as addition on standard numbers can only give standard numbers and addition on subnormals is exact, the absolute part of the bound should not be necessary here. However, this reasoning is currently out of reach of the underlying SMT solvers.
- 8.
References
Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point Java programs in KeY. In: TACAS (2), pp. 242–261 (2021)
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification-the key book. Lecture Notes in Computer Science, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6
Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3(OOPSLA), 1–30 (2019)
Barnes, J.: Programming in Ada 2012. Cambridge University Press, Cambridge (2014)
Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64 (2011)
Boldo, S.: Formal verification of programs computing the floating-point average. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 17–32. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_2
Boldo, S., Marché, C.: Formal verification of numerical programs: from c annotated programs to mechanical proofs. Math. Comput. Sci. 5(4), 377–393 (2011)
Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243–252. IEEE (2011)
Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 79–98. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_5
Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35
Conchon, S., Iguernlala, M., Ji, K., Melquiond, G., Fumex, C.: A three-tier strategy for reasoning about floating-point numbers in SMT. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 419–435. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_22
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16
De Dinechin, F., Lauter, C., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60(2), 242–253 (2010)
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). https://doi.org/10.1007/978-3-642-04570-7_6
Dross, C., Moy, Y.: Auto-active proof of red-black trees in SPARK. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 68–83. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_5
Fumex, C., Marché, C., Moy, Y.: Automating the verification of floating-point programs. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 102–119. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_7
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4
Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010)
Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: European Symposium on Programming, pp. 484–514. Springer, Cham (2020)
McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)
Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. (TOPLAS) 30(3), 1–41 (2008)
Moscato, M.M., Titolo, L., Feliú, M.A., Muñoz, C.A.: Provably correct floating-point implementation of a point-in-polygon algorithm. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 21–37. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_3
Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT), p. 151 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Dross, C., Kanig, J. (2022). Making Proofs of Floating-Point Programs Accessible to Regular Developers. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds) Software Verification. NSV VSTTE 2021 2021. Lecture Notes in Computer Science(), vol 13124. Springer, Cham. https://doi.org/10.1007/978-3-030-95561-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-95561-8_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-95560-1
Online ISBN: 978-3-030-95561-8
eBook Packages: Computer ScienceComputer Science (R0)