Deductive verification of floating-point Java programs in KeY

DOI10.1007/978-3-030-72013-1_13MaRDI QIDQ2233510zbMATH OpenOpenAlexFDO

Authors Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.08733

zbMATH Keywords

floating-point arithmeticdeductive verificationtranscendental functions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• Multi-prover verification of floating-point programs
• Automating the verification of floating-point programs
• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• A two-phase approach for conditional floating-point verification
• Verified compilation of floating-point computations

Cites work

• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 1852915 (Why is no real title available?)
• A formal analysis of the compact position reporting algorithm
• A parameterized floating-point formalizaton in HOL Light
• Automatic detection of floating-point exceptions
• Automating the verification of floating-point programs
• Building high integrity applications with SPARK
• Certified roundoff error bounds using semidefinite programming
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Handbook of Floating-Point Arithmetic
• MetiTarski: An automatic theorem prover for real-valued special functions
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Sound compilation of reals
• Static analysis of finite precision computations
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• The MathSAT5 SMT solver
• Viper: a verification infrastructure for permission-based reasoning
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• dReal: an SMT solver for nonlinear theories over the reals

Cited in

(3)

• Automating the verification of floating-point programs
• Multi-prover verification of floating-point programs
• Model checking linear dynamical systems under floating-point rounding

Describes a project that uses

Uses Software

• Daisy
• Nagini
• QF_FP
• JBMC
• OpenJML
• Viper
• KeY
• MathSAT5
• CVC4
• Boogie
• VeriFast
• dReal
• Flocq
• HOL Light
• HOL
• z3
• Frama-C
• Why3
• SMT-LIB
• KRAKATOA
• MetiTarski
• Coq
• Apron

This page was built for publication: Deductive verification of floating-point Java programs in KeY

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233510)