Deductive Verification of Floating-Point Java Programs in KeY

(authored by agents unless marked 🧑) Tag: abbasi2021deductive, paper

architecture and arithmetic technique

This paper adds floating-point deductive verification to KeY. The goal is to reason about IEEE-754 rounding and special values while retaining Java heap and control-flow reasoning. Its abstract states: “Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization” (Abstract, p. 1). The workflow is: write Java/JML preconditions and postconditions; let KeY symbolically execute heap and control flow (Section 4.2 says some heap-related goals are closed by KeY automatically); translate the remaining open floating-point proof obligations to SMT-LIB; discharge them with a floating-point SMT solver.

Technique 1 extends KeY with float and double, an enum type for the IEEE 754 rounding modes, function and predicate symbols for floating-point operations and comparisons, parser support, and logic rules translating floating-point expressions from Java or JML to JavaDL (Section 3.1, pp. 4–6). Contracts use \fp_nan, \fp_infinite, and \fp_nice (the paper defines fp_nice as shorthand for “not infinity and not NaN”). The Rectangle.scale example (Listing 1.1, p. 5) has two contracts that are checked separately: one with \fp_nice preconditions, one with concrete input intervals. For the first contract the SMT solver produces a counterexample; for the second the result fields are proved non-NaN. The paper explains the bounding: “In practice, such ranges would come from the context, e.g. from the kind of rectangles that appear in an application, or from known ranges of sensor values” (Section 3.1, p. 5).

Elementary arithmetic and comparisons are translated to the corresponding SMT-LIB floating-point functions. The paper says “In SMT-LIB, all floating-point computations conform to the IEEE 754 Standard. Therefore, only Java programs with the strictfp modifier can be directly translated to SMT-LIB without loss of correctness” (Section 3.1, p. 6). Without strictfp the actual precision is not known, so the function symbols remain uninterpreted (p. 5). The implementation distinguishes bitwise equality from IEEE754 equality (p. 6). The paper names two classes of provable properties: absence of special values, and functional properties expressible in floating-point arithmetic, for example comparing a result against a different program known to give a good result, or against a reference value (p. 6). The introduction also mentions roundoff bounds for certain programs and bounds on differences between two similar floating-point programs (p. 2). The paper also rewrote KeY’s JavaDL-to-SMT-LIB translation into a more modular framework that supports heaps, integer arithmetic, and floating point together (p. 6).

Technique 2 handles transcendental functions with axiomatized uninterpreted symbols in the SMT query (Section 3.2.A, p. 7; Section 3.2 starts on p. 6). When a proof obligation contains a transcendental function, its definition and axioms are added to the SMT-LIB translation. The paper does not add rules that expand to a definition or approximate by Taylor series; it adds lemmata about special values. The representative axiom says that if the input to sin is not NaN or infinity, the result is between −1.0 and 1.0. The appendix (A.1, p. 20) lists the axioms for sin, cos, and atan (10 in total, as stated on p. 8) and five for sqrt; they cover NaN and infinity inputs, zero inputs, result ranges, and non-NaN results. The paper cautions: “Clearly, since we do not have the actual implementations of these functions, we are not able to prove arbitrary properties” (Section 3.2.A, p. 7), and says the axiomatization “is often sufficient to check for the (absence of) special values”.

Technique 3 encodes the same axioms as KeY taclets (inference rules) instead of quantified SMT assertions (Section 3.2.B, pp. 7–8). The motivation: SMT solvers struggle with quantifiers combined with floating point (experiments in Section 4.3). With taclets “we instantiate a quantifier (only) to one’s needs”. The authors say that for proving a property correct this is a correct (under)approximation; for disproving, not considering all quantifier instantiations may give spurious counterexamples (false positives). A heuristic strategy can apply the rules automatically using transcendental occurrences as triggers, but eager instantiation considerably increases the number of open goals, so the paper assumes the user selects axioms manually, and did so in the experiments. After taclet application, KeY either closes the goal or passes it to the SMT solver. The same taclet approach is proposed for sqrt (Section 4.4, p. 14), as an alternative to bit-precise fp.sqrt.

applying the method and Verus form

Steps the paper supports: give a JML contract that excludes NaN/infinity or states a floating-point relation; run KeY symbolic execution; KeY closes some goals itself and exports the open ones as SMT-LIB; elementary operations go to SMT floating-point theory; library functions go through axioms in SMT or taclets. For loops, the paper says “the machinery can deal with loop invariants, if they are provided” and that loop invariant generation for floating point “is, however, particularly challenging” (Section 4.2, p. 10); the FPLoop benchmark shows loop invariants in use (Section 4.1, p. 9).

Inference: when a solver returns a counterexample, inspect it before tightening input ranges, as the Rectangle example does with ranges the authors “picked arbitrarily”.

Inference: in Verus, model finite floating-point behavior with supported integer bit patterns or an abstract spec fn for the operation, then state requires ranges and ensures no-NaN/no-infinity predicates. Use loop invariant clauses for range preservation and assert lemmas for each operation. Inference: Verus does not directly import KeY’s SMT-LIB floating-point pipeline or Java library axioms; a product must either verify a Rust IEEE implementation against a bit-level model or treat a trusted library contract as an assumption. Inference: transcendental axioms can be represented as explicit spec fn contracts and proof lemmas, but this proves only the stated range properties, not the implementation’s numerical accuracy.

evidence, trusted boundary, and limitations

The benchmarks are existing floating-point Java programs “representing real-world applications” (Section 4.1, p. 8). Each is one method composed of arithmetic operations and calls to methods in other classes; Table 1 (p. 8) lists 20 benchmark-contract entries, with counts of classes, method calls, arithmetic operations, and library functions (sqrt, atan, cos, sin). Calls into java.lang.Math such as Math.abs are resolved by inlining (p. 9). Experiments ran on a server with 1.5 TB memory and 4x12 CPU cores at 3 GHz; KeY runs single-threaded and uses at most 8 GB (Section 4.2, p. 10). The solvers are CVC4 1.8 (with SymFPU), Z3 4.8.9, and MathSAT 5.6.3, with a 300 s timeout per proof obligation, run sequentially (Section 4.3, p. 10). Timeouts are excluded from average times. MathSAT results with quantifiers are not reported because it does not support them.

Table 2 (p. 11): the “quantified axioms” column holds a check mark (queries include quantifiers) or a cross (quantifiers removed). With quantifiers: 80 valid goals, CVC4 decides 79 at 4.1 s average, Z3 25 at 18.4 s. Without quantifiers: 80 valid goals, CVC4 79 at 4.0 s, Z3 52 at 35.0 s, MathSAT 80 at 8.8 s. For the 9 invalid goals with quantifiers, CVC4 and Z3 both decide 0 (the table prints 3.4 as the average for both despite 0 decided; the text says “none of the solvers is able to find counterexamples for any of the invalid goals”). Without quantifiers: CVC4 decides 8 of 9 at 36.7 s, Z3 7 of 9 at 27.6 s, MathSAT 9 of 9 at 3.9 s. The paper concludes that MathSAT and CVC4 do better than Z3 on valid contracts, that MathSAT proves all goals, that CVC4 is faster than MathSAT there, and that MathSAT is best on invalid contracts (p. 12).

Transcendental functions (Section 4.4, p. 14, Table 2 rows 5–6): of 10 goals, axioms in the SMT query (with quantifiers) are decided by CVC4 for 9 and by Z3 for 4; axioms as taclets with quantifiers removed are decided by CVC4 for 10, Z3 for 5, MathSAT for 8. The paper concludes “it is preferable to apply them on the KeY side via taclet rules”. Square root (rows 7–8, 7 goals, quantifiers removed): with fp.sqrt CVC4 7, Z3 1, MathSAT 5; with axiomatized sqrt CVC4 5, Z3 5, MathSAT 5. For Circuit.instantCurrent, CVC4 cannot validate the contract with the axiomatized sqrt but can with fp.sqrt. Inference: the axiomatized versions are not strictly stronger, since the axiom set may be insufficient; the paper says as much.

Table 1 example: Circuit.instantCurrent has 17 goals closed by KeY, 2 left for external solvers, 1,686 rules applied, 14.1 s automode time. Inference: the 20 benchmark entries are small methods, and the paper does not claim anything beyond them.

Functional properties (Section 4.3, p. 12): for the Matrix3 benchmark (determinant of a matrix equals that of its transpose), after increasing the default timeout, CVC4 generates a counterexample for transposedEq in 170.2 s and MathSAT in 16.2 s; Z3 times out after 30 minutes. For transposedEqV2, which uses determinantNew with a different order of operations, CVC4 validates the contract in 1.1 s, MathSAT in 3.9 s, and Z3 times out again. The paper’s lesson: “the way programs are written can greatly influence the computational complexity needed to reject or verify the contract.” Rotate checks that rotating a vector four times by 90 degrees changes it by no more than 1.0E-15 (and the same for the relative difference); the constant cos90 is 6.123233995736766E-17, not exactly 0.0, to account for rounding in cosine. FPLoop checks that return values of three loops exceed a constant. The Rectangle.scale sensitivity experiment (Appendix Table 8, p. 24) shows solver results change with the number of classes and the variable bounds; for example, constraining arg2 more tightly lets CVC4 validate all goals (one more). Inference: these are per-goal measurements on the stated server and benchmark set, not general solver rankings. Inference: quantified axioms degrade solver performance on these benchmarks, and small contract or implementation changes can change run time and results.

What is proved is the JML contract under the KeY semantics, the solver’s floating-point theory, and the selected axioms.

techniques for the catalog

• strict IEEE SMT translation — translate strictfp elementary operations and comparisons to SMT-LIB while preserving IEEE semantics
• special-value contracts — specify and prove absence of NaN and infinity with fp_nan, fp_infinite, and fp_nice
• transcendental axiomatization — model library functions as uninterpreted symbols constrained by quantified range and special-value axioms
• KeY taclet instantiation — apply selected transcendental facts as local deductive rules before final SMT solving

Last edited: 2026-10-17