Deductive verification of floating-point Java programs in KeY. (English) Zbl 1474.68186
Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
Summary: Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and ‘Not a Number’ (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values – often a prerequisite for further reasoning about numerical computations – as well as certain functional properties for realistic benchmarks.
For the entire collection see [Zbl 1471.68016].
For the entire collection see [Zbl 1471.68016].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 65G50 | Roundoff error |
| 68N15 | Theory of programming languages |
Software:
OpenJML; JBMC; Daisy; Viper; MetiTarski; QF_FP; Boogie; Why3; Flocq; Coq; Apron; z3; KeY; SMT-LIB; KRAKATOA; VeriFast; HOL; Frama-C; dReal; MathSAT5; Nagini; CVC4; HOL LightReferences:
| [1] | QF \(\_\) FP SMT benchmarks. https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_FP (2019) |
| [2] | Slow verification of programs combining multiple floating point values (Github issue) (2019 (accessed May 11, 2020)), https://github.com/boogie-org/boogie/issues/109 |
| [3] | Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive Verification of Floating-Point Java Programs in KeY. CoRR abs/2101.08733 (2021) |
| [4] | Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, LNCS, vol. 10001. Springer (2016) |
| [5] | Akbarpour, B., Paulson, L.C.: MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. Journal of Automated Reasoning 44(3) (2010) · Zbl 1215.68206 |
| [6] | Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging Rust Types for Modular Specification and Verification. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (2019) |
| [7] | Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic Detection of Floating-point Exceptions. In: Principles of Programming Languages (POPL) (2013) · Zbl 1301.68087 |
| [8] | Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi’c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Computer Aided Verification (CAV) (2011), snowbird, Utah |
| [9] | Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB Standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010) |
| [10] | Beckert, B., Nestler, B., Kiefer, M., Selzer, M., Ulbrich, M.: Experience Report: Formal Methods in Material Science. CoRR abs/1802.02374 (2018) |
| [11] | Benz, F., Hildebrandt, A., Hack, S.: A Dynamic Program Analysis to Find Floating-Point Accuracy Problems. In: Programming Language Design and Implementation (PLDI) (2012) |
| [12] | Beyer, D.: Advances in automatic software verification: Sv-comp 2020. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2020) |
| [13] | Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Programming Language Design and Implementation (PLDI) (2003) · Zbl 1026.68514 |
| [14] | 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) (2013) · Zbl 1267.68208 |
| [15] | Boldo, S., Filliâtre, J.C., Melquiond, G.: Combining Coq and Gappa for Certifying Floating-Point Programs. In: Intelligent Computer Mathematics (2009) · Zbl 1247.68232 |
| [16] | Boldo, S., Melquiond, G.: Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. In: IEEE Symposium on Computer Arithmetic (ARITH) (2011) |
| [17] | Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. In: IEEE Symposium on Computer Arithmetic (ARITH) (2015) |
| [18] | Brain, M., Schanda, F., Sun, Y.: Building Better Bit-Blasting for Floating-Point Problems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019) |
| [19] | Chapman, R., Schanda, F.: Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. In: Interactive Theorem Proving (ITP) (2014) |
| [20] | Chen, L., Miné, A., Cousot, P.: A Sound Floating-Point Polyhedra Abstract Domain. In: Asian Symposium on Programming Languages and Systems (APLAS) (2008) |
| [21] | Chiang, W.F., Gopalakrishnan, G., Rakamaric, Z., Solovyev, A.: Efficient Search for Inputs Causing High Floating-point Errors. In: Principles and Practice of Parallel Programming (PPoPP) (2014) |
| [22] | Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2013) · Zbl 1381.68153 |
| [23] | Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: NASA Formal Methods (2011) |
| [24] | Cordeiro, L.C., Kesseli, P., Kroening, D., Schrammel, P., Trtík, M.: JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. In: Computer Aided Verification (CAV) (2018) |
| [25] | Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Software Engineering and Formal Methods (SEFM) (2012) |
| [26] | Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy - Framework for Analysis and Optimization of Numerical Programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2018) |
| [27] | Darulova, E., Kuncak, V.: Towards a Compiler for Reals. TOPLAS 39(2) (2017) · Zbl 1284.68393 |
| [28] | De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2008) |
| [29] | Eilers, M., Müller, P.: Nagini: A Static Verifier for Python. In: Computer Aided Verification (CAV) (2018) |
| [30] | Filliâtre, J.C., Paskevich, A.: Why3 — Where Programs Meet Provers. In: European Symposium on Programming (ESOP) (2013) |
| [31] | Fox, A., Harrison, J., Akbarpour, B.: A Formal Model of IEEE Floating Point Arithmetic. HOL4 Theorem Prover Library (2017), https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/floating-point |
| [32] | Fumex, C., Marché, C., Moy, Y.: Automating the Verification of Floating-Point Programs. In: Verified Software: Theories, Tools, and Experiments (VSTTE) (2017) · Zbl 1403.68223 |
| [33] | Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT Solver for Nonlinear Theories over the Reals. In: Automated Deduction - CADE-24 (2013) · Zbl 1381.68268 |
| [34] | Ge, Y., de Moura, L.: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In: Computer Aided Verification (CAV) (2009) · Zbl 1242.68280 |
| [35] | Goubault, E., Putot, S.: Static Analysis of Finite Precision Computations. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2011) · Zbl 1317.68116 |
| [36] | Goubault, E., Putot, S.: Robustness Analysis of Finite Precision Implementations. In: Asian Symposium on Programming Languages and Systems (APLAS) (2013) · Zbl 1317.68116 |
| [37] | Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. In: Handbook of Philosophical Logic, pp. 99-217. Springer (2001) · Zbl 1003.03528 |
| [38] | Harrison, J.: Floating Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3) (2000) |
| [39] | IEEE, C.S.: IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (2008) |
| [40] | Izycheva, A., Darulova, E., Seidl, H.: Counterexample and Simulation-Guided Floating-Point Loop Invariant Synthesis. In: Static Analysis Symposium (SAS) (2020) · Zbl 1474.68055 |
| [41] | Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: NASA Formal Methods (NFM) (2011) |
| [42] | Jacobsen, C., Solovyev, A., Gopalakrishnan, G.: A Parameterized Floating-Point Formalizaton in HOL Light. Electronic Notes in Theoretical Computer Science 317 (2015) · Zbl 1352.65667 |
| [43] | Jeannet, B., Miné, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Computer Aided Verification (CAV) (2009) |
| [44] | Lam, M.O., Hollingsworth, J.K., Stewart, G.W.: Dynamic Floating-point Cancellation Detection. Parallel Comput. 39(3) (2013) |
| [45] | Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes 31(3) (2006) |
| [46] | Leavens, G.T., Cheon, Y.: Design by Contract with JML (2006), http://www.jmlspecs.org/jmldbc.pdf |
| [47] | Leino, K.R.M.: This is Boogie 2 (June 2008), https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/ |
| [48] | Magron, V., Constantinides, G., Donaldson, A.: Certified Roundoff Error Bounds Using Semidefinite Programming. ACM Trans. Math. Softw. 43(4) (2017) · Zbl 1380.65084 |
| [49] | Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of Java/JavaCard programs annotated in JML. The Journal of Logic and Algebraic Programming 58(1) (2004) · Zbl 1073.68678 |
| [50] | McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press (2015) · Zbl 1328.68009 |
| [51] | Meyer, B.: Applying “Design by Contract”. Computer 25(10) (1992) |
| [52] | Moscato, M., Titolo, L., Dutle, A., Muñoz, C.: Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. In: SAFECOMP (2017) · Zbl 1403.68324 |
| [53] | Muller, J., Brisebarre, N., de Dinechin, F., Jeannerod, C., Lefèvre, V., Melquiond, G., Revol, N., Stehlé, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkhäuser (2010) · Zbl 1197.65001 |
| [54] | Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A Verification Infrastructure for Permission-Based Reasoning. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2016) · Zbl 1475.68191 |
| [55] | Pasareanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: International Symposium on Software Testing and Analysis (ISSTA) (2008) |
| [56] | Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs. In: International Symposium on Software Testing and Analysis (ISSTA) (2006) |
| [57] | Solovyev, A., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In: Formal Methods (FM) (2015) · Zbl 1427.65064 |
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.
