1 Introduction
sqrt(1.0)
result in a Not a Number (NaN) value. These special values are problematic as seemingly straightforward identities do not hold (x == x
or x * 0.0 == 0.0
). In addition, every operation on floatingpoint numbers potentially involves rounding, which compromises familiar rules like associativity and distributivity. Hence, reasoning support for writing correct floatingpoint programs is indispensable.
we implement and evaluate the first automated deductive verification of floatingpoint Java programs by combining the strength of rulebased and SMTbased deduction;

we develop novel automated support for reasoning about transcendental functions in a deductive verifier;

we add support for reasoning about (potentially rounding) type conversions;

we collect a new set of challenging realworld floatingpoint benchmarks in Java;^{1}

we compare different SMT solvers for discharging floatingpoint VCs on this new set of benchmarks.
sqrt
, new rules—and accordingly experiments—for (potentially rounding) casts between integers and floats, new experiments on the verification of floatingpoint loop invariants, new experiments on the sensitivity of SMT solvers to numerous problem modifications, and extended reporting of the experiments presented in [1].2 Background
2.1 Introduction to KeY
find
term \(t_{ find }\) which has to match an expression or formula in the current goal, and a term \(t_{ replace }\) which replaces the matched expression or formula. New formulas may be introduced as new assumptions onto the proof goal using add
. If the rule has a side condition \(\varphi _{ show }\) that needs to be established, it can be optionally specified using show
that will open a new proof goal for \(\varphi _{show}\). One of the clauses for add
and replace
may be empty or omitted. The taclet language supports typed metavariables and heuristics for KeY ’s automation.2.2 Floatingpoint arithmetic in Java
float
and double
. They are associated with the 32bit and 64bit format, respectively, as specified in the IEEE 754 Standard for FloatingPoint Arithmetic. More precisely, Java implements a subset of that standard. In the following, we summarize some central characteristics of Java floatingpoint numbers, loosely following Muller et.al. [52]. Most of this is not specific to Java, but more generally applies to IEEE 754. Note that the Java Virtual Machine (JVM) only supports floatingpoint numbers with base 2, even if the Java language syntax supports base 10 as well, in such a way that parsing and input/output routines translate back and forth between the bases.float
with \(p = 24\), \(e_{min} = 126, e_{max} = 127\) and double
with \(p = 53, e_{min} = 1022, e_{max} = 1023\).float
has a significand of 24 bits and can therefore not exactly represent all integers of the 32bit type int
. However, integers whose absolute value is smaller than \(2^{24}\) can be represented in an exact way in the type float
.==
\(0.0\) and \(0.0\)==
\(+0.0\) both return true
. If the absolute value of the ideal result of a computation is too small to be representable as a floatingpoint number of the given format, the resulting floating point number is \(+0\) or \(0\). In addition, there are three special values, \(+\infty \), \(\infty \), and NaN (Not a Number). If the absolute value of the ideal result of a computation is too big to be representable as a floatingpoint number of the given format, the result is \(+\infty \) or \(\infty \). Also, division by zero will give an infinite result (e.g., \(7.3/+0=+\infty \)).^{3} Computing further with infinity may give an infinite result (e.g., \(+\infty + +\infty = +\infty \)), but may also result in the additional ‘error value’ NaN (e.g., \(+\infty  +\infty = \text {NaN}\)). The predicates
return false
as soon as one operand evaluates to NaN. The predicate !=
returns true
as soon as one operand evaluates to NaN. In particular, NaN==
NaN returns false
, and NaN!=
NaN returns true
. Due to the presence of infinities and NaN, floatingpoint operations do not throw Java exceptions.^{4}strictfp
modifier, ensuring that floatingpoint computations inside methods or classes with the strictfp
modifier comply to the precision defined in the IEEE 754 Standard, even for intermediate results. This modifier ensures portability. Additionally, one can set the Assume strictfp option in KeY, meaning that all computations are assumed to be within the scope of a strictfp
modifier, even if strictfp
is not explicit in the code.3 Floatingpoint support in KeY
3.1 Arithmetics
float
and double
types to the KeY type system, introduced functions and predicate symbols to formalize arithmetic operations (+
, *
, ...), and comparisons (
, ==
, ...) on floatingpoint expressions, and added cast operations among floatingpoint and integer types ((double)
, (float)
, (int)
). The translation supports both code with and without the strictfp
modifier. However, since the actual precision of nonstrictfp operations is not known, the function symbols remain uninterpreted. We assume that the strictfp
modifier is set for all our benchmarks. We extended KeY ’s parser to correctly handle programs and annotations containing floatingpoint numbers and added logic rules for translating floatingpoint expressions from Java or JML to JavaDL.Rectangle
benchmark that contains floatingpoint literals and makes use of the fp_nan
and fp_nice
predicates. fp_nan
states that a floatingpoint expression is NaN and fp_nice
, states that a floatingpoint expression is neither NaN nor infinity. The scale
method contains two contracts that are checked separately, ensuring that the class fields of a scaled rectangle object are not NaN, considering different preconditions. For the first contract, the SMT solver produces a counterexample. In the second, we bound inputs by concrete ranges that we picked arbitrarily and get the valid result. 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.strictfp
modifier can be directly translated to SMTLIB without loss of correctness.fp_nan
and fp_infinite
predicates (or the fp_nice
equivalent). Furthermore, one can specify functional properties (including loop invariants) that are expressible in floatingpoint arithmetic, e.g., one can compare the result of a computation against the result of a different program which is known to produce a good result or a reference value.3.2 Transcendental functions
sin
and cos
. In Java programs, these functions are implemented as static library functions in the class java.lang.Math
.3.2.1 Axiomatization in SMT
sin
function is not a NaN or infinity, then the returned value of sin
is between \(1.0\) and 1.0:
3.2.2 Taclets in KeY
3.3 Interaction of floats with other primitive types
float
or double
. Our SMT translation in KeY does not only target the floatingpoint theory, but encodes other aspects of proof obligations into theories like linear integer arithmetic for integers, or arrays representing heap data structures. In the evaluation, the stateoftheart SMT solvers show their ability to reason about these theories when they occur simultaneously within the same proof obligation. As long as the different theories act on disjoint domains, this combined integrated translation works nicely in most cases. For instance, programs using float
arrays or class attributes of type double
can be handled as long as floatingpoint values and other types are not arithmetically combined within an expression.float
value, yielding a float
value. Such cases of intersecting value domains require special attention.int
values which can be represented in float
without loss of precision. In particular, all integers between \(2^{24}\) and \(2^{24}\) are floatrepresentable.^{5} According to the Java Language Specification (JLS) [33], an implicit widening cast called numeric promotion is applied when different primitive types are combined in an arithmetic operation. The addition iv + fv
of an integer variable iv
and a float
variable fv
is hence equivalent to the expression (float)iv + fv
in which the numeric promotion has been made explicit.float
s. Since this family of cast operators on primitive types is translated from JML into JavaDL as uninterpreted functions, we can build a bridge between the integer and floatingpoint domains by adding theorems/axioms about the numeric promotion to KeY in form of taclets.float
and then back to an int
is the identity if i stays within the range of floatrepresentable values.int
overflow. Then, \(\mathtt {(float)}(a+b) = \mathtt {(float)}a + \mathtt {(float)}b\).float
on the left of the equation. At the same time, the float
addition on the right side of the equation may also require rounding. The insight from the proof above is that the IEEE standard and the JLS force the rounding on both sides to be the same!float
side, like
double
and long
.4 Evaluation
4.1 Benchmark programs
Benchmark  Benchmark details  Automode statistics  

# Classes  # Method calls  # Arith. ops  Library functions  # Goals closed by KeY  # Goals to be closed externally  # Rules applied  Automode time (s)  
Complex.add (2)  1  0  2  –  3 / 3  1 / 4  185 / 286  0.7 / 0.2 
Complex.divide (2)  1  0  11  –  10 / 8  2 / 8  483 / 625  0.7 / 0.8 
Complex.compare  1  0  2  –  3  2  216  0.2 
Complex.reciprocal (2)  1  1  6  –  1 / 1  2 / 2  402 / 406  0.4 / 0.5 
Circuit.impedance  2  1  3  –  1  4  360  0.5 
Circuit.current (2)  2  3  14  –  11 / 11  4 / 1  1267 / 1238  4.0 / 4.1 
Matrix2.transposedEq  1  3  3  –  3  1  735  0.9 
Matrix3.transposedEq  1  4  34  –  3  1  1786  5.1 
Matrix3.transposedEqV2  1  4  34  –  3  1  1796  5.4 
Rectangle.scale (2)  3 + 1  23  22  –  32 / 32  32 / 16  5990 / 5617  18.4 / 14.5 
Rotate.computeError  1 + 1  6  26  –  108  8  3693  74.2 
Rotate.computeRelErr  1 + 1  6  28  –  120  8  3898  79.6 
FPLoop.fploop  1  0  1  –  2  4  99  0.1 
FPLoop.fploop2  1  0  1  –  2  4  99  0.1 
FPLoop.fploop3  1  0  1  –  2  4  99  0.1 
Pine.ex2  1  1  9  –  2  12  320  1.3 
Pine.ex2reset  1  1  9  –  2  16  394  1.8 
Pine.ex3resetleadlag  1  1  6  –  2  15  240  0.5 
Pine.ex7dampened  1  1  5  –  2  10  203  0.6 
Pine.filtergoubault  1  1  3  –  2  8  183  0.5 
Pine.filtermine1  1  1  4  –  2  10  211  0.6 
Pine.filtermine2  1  1  3  –  2  8  172  0.6 
Pine.filtermine2nondet  1  1  4  –  2  8  193  0.5 
Pine.harmonic  1  1  5  –  2  9  199  0.4 
Pine.pendulumapprox  1  1  17  –  2  10  299  0.9 
Pine.pendulumsmall  1  1  7  –  2  10  224  0.7 
Pine.symplectic  1  1  6  –  2  9  195  0.7 
Cartesian.toPolar  2 + 1  3  6  sqrt, atan  1  4  438  0.5 
Cartesian.distanceTo  1 + 1  1  5  sqrt  2  1  191  0.1 
Polar.toCartesian  2 + 1  3  4  cos, sin  1  2  364  0.5 
Circuit.instantCurrent  2 + 1  14  23  sqrt, atan, cos  17  2  1686  14.1 
Circuit.instantVoltage  1 + 1  1  4  cos  0  2  138  0.1 
java.lang.Math
(e.g., Math.abs
) are marked by “+1” in Table 1; these are resolved by inlining the method implementation. For benchmarks that contain calls to transcendental functions and square root, the called functions are listed; these are handled by our axiomatization. We include sqrt
in this list, as we have observed that exact support can be expensive, so it may be advantageous to handle sqrt
axiomatically. We include benchmarks with loops and loop invariants used for the evaluation of the tool
[39], represented as Pine.*
. Benchmarks Rectangle
, Circuit
, Matrix3
, Rotation
and Pine.pendulumapprox
are partially shown in Listings 1, 6, 3, 4 and 5 respectively.Details  Experiment  Quantified axioms  # Goals  CVC4  Z3  MathSAT  

# Goals decided  Avg.  # Goals decided  Avg.  # Goals decided  Avg.  
Table 3  Valid contracts  ✓  80  79  5.4  25  25  –  – 
Table 4  ✗  80  79  5.3  52  63.7  80  10.1  
Table 5  Invalid contracts  ✓  9  0  7.6  0  2.6  –  – 
✗  9  8  12.8  7  60.4  9  2.0  
Table 8  Axioms in SMT  ✓  10  9  17.3  4  65.0  –  – 
Axioms as taclets  ✓  10  10  28.0  2  164.0  –  –  
Axioms as taclets  ✗  10  10  28.1  5  84.3  8  1.5  
Table 9  fp.sqrt  ✗  7  7  40.4  1  23.5  5  1.2 
Axiomatized sqrt  ✗  7  5  2.1  5  86.4  5  3.9  
Table 6  Loop invariants  ✗  113  113  6.5  112  13.5  113  5.0 
Matrix
, FPLoop
, Rotate
and Pine.*
benchmarks, we check a functional property (see Sect. 4.3). The Pine.*
benchmarks and FPLoop
, which has three contracts, additionally show how to specify floatingpoint loop behavior using loop invariants.4.2 Proof obligation generation
4.3 Evaluation of SMT floatingpoint support
Benchmark  # Goals  CVC4  Z3  

# Goals proven  Avg.  Max.  # Goals proven  Avg.  Max.  
Complex.add(1)  1  1  0.6  0.6  1  1.6  1.6 
Complex.divide(1)  2  2  1.7  1.9  2  1.8  2.3 
Complex.divide(2)  8  8  3.4  11.5  4  3.2  TO 
Complex.compare  2  2  0.5  0.6  2  1.5  1.5 
Complex.reciprocal(1)  2  2  1.0  1.7  0  –  TO 
Complex.reciprocal(2)  2  2  1.8  2.4  2  2.7  4.0 
Circuit.impedance  4  4  0.8  0.9  3  87.5  TO 
Circuit.current(1)  4  4  6.3  13.2  0  –  TO 
Circuit.current(2)  1  1  5.5  5.5  0  –  TO 
Matrix2.transposedEq  1  1  0.5  0.5  0  –  TO 
Matrix3.transposedEqV2  1  1  1.3  1.3  0  –  TO 
Rectangle.scale(1)  32  31  2.2  TO  7  46.6  TO 
Rotate.computeError  8  8  9.8  13.9  0  –  TO 
Rotate.computeRelErr  8  8  25.3  45.6  0  –  TO 
FPLoop.fploop  4  4  0.5  1.0  4  2.3  8.1 
Summary  80  79  5.4  TO  25  25  TO 
Benchmark  # Goals  CVC4  Z3  MathSAT  

# Goals proven  Avg.  Max.  # Goals proven  Avg.  Max.  # Goals proven  Avg.  Max.  
Complex.add(1)  1  1  0.5  0.5  1  1.3  1.3  1  0.2  0.2 
Complex.divide(1)  2  2  1.6  1.9  2  2.1  2.7  2  1.5  1.9 
Complex.divide(2)  8  8  3.4  11.4  4  2.5  TO  8  29.0  209.5 
Complex.compare  2  2  0.5  0.6  2  1.1  1.3  2  0.2  0.2 
Complex.reciprocal(1)  2  2  0.9  1.5  1  198.5  TO  2  2.2  2.4 
Complex.reciprocal(2)  2  2  1.7  2.3  2  2.8  3.4  2  1.5  1.9 
Circuit.impedance  4  4  0.7  0.7  4  9.5  17.1  4  0.4  0.5 
Circuit.current(1)  4  4  6.3  13.0  0  –  TO  4  13.3  36.2 
Circuit.current(2)  1  1  5.2  5.2  0  –  TO  1  26.3  26.3 
Matrix2.transposedEq  1  1  0.5  0.5  0  –  TO  1  0.6  0.6 
Matrix3.transposedEqV2  1  1  1.1  1.1  0  –  TO  1  3.9  3.9 
Rectangle.scale(1)  32  31  2.1  TO  32  95.1  251.8  32  2.4  4.2 
Rotate.computeError  8  8  9.7  13.5  0  –  TO  8  22.7  35.7 
Rotate.computeRelErr  8  8  25.0  45.0  0  –  TO  8  27.5  46.4 
FPLoop.fploop  4  4  0.5  1.1  4  2.0  7.2  4  0.4  1.0 
Summary  80  79  5.3  TO  52  63.7  TO  80  10.1  209.5 
Benchmark  # Goals  CVC4  Z3  MathSAT  

# Goals  Avg.  Max.  # Goals  Avg.  Max.  # Goals  Avg.  Max.  
Valid  Invalid  Valid  Invalid  Valid  Invalid  Valid  Invalid  
With quantified axioms  
Matrix3.transposedEq  0  1  0  0  –  TO  0  0  –  TO  –  –  –  – 
Rectangle.scale(2)  12  4  12  0  12.2  TO  8  0  4.6  TO  –  –  –  – 
Complex.add(2)  2  2  2  0  0.6  0.7  2  0  1.4  TO  –  –  –  – 
FPLoop.fploop2  3  1  3  0  0.9  1.7  3  0  0.5  TO  –  –  –  – 
FPLoop.fploop3  3  1  3  0  0.4  1.7  3  0  0.3  TO  –  –  –  – 
Summary  20  9  20  0  7.6  TO  16  0  2.6  TO  –  –  –  – 
Without quantified axioms  
Matrix3.transposedEq  0  1  0  1  170.2  170.2  0  0  –  TO  0  1  16.2  16.2 
Rectangle.scale(2)  12  4  12  3  12.2  TO  12  3  108.2  TO  12  4  2.4  9.5 
Complex.add(2)  2  2  2  2  0.5  0.5  2  2  0.7  1.0  2  2  0.2  0.2 
FPLoop.fploop2  3  1  3  1  0.4  0.6  3  1  0.9  1.7  3  1  0.3  0.5 
FPLoop.fploop3  3  1  3  1  0.3  0.6  3  1  0.6  1.7  3  1  0.2  0.4 
Summary  20  9  20  8  12.8  TO  20  7  60.4  TO  20  9  2.0  16.2 
Matrix
, we check that the determinants of a matrix and its transpose are equal. Note that this property holds trivially under real arithmetic, but not necessarily under floatingpoints. After feeding transposedEq
(which uses the determinant
method) and its contract to KeY, increasing the default timeout sufficiently and discharging the created goal, CVC4 generates a counterexample in 170.2s seconds and MathSAT in 16.2s. Z3 times out after 30 minutes. By feeding transposedEqV2
(which uses the determinantNew
method) to KeY, CVC4 validates the contract in 1.1s, MathSAT in 3.9s and Z3 times out again. One thing worth noting is that the way programs are written can greatly influence the computational complexity needed to reject or verify the contract. This is evident from the fact that slightly modifying the order of operations (using determinantNew
instead) substantially reduces verification time and changes the verification result for MathSAT and CVC4.Rotate
, we check that the difference between an original vector and the one that is rotated four times by 90 degrees must not be larger than 1.0E15. We also verified the same bound for the relative difference (by exploiting another method and contract) for this benchmark. The constant cos90
in Listing 4 is not precisely 0.0 to account for rounding effects in the computation of the cosine. FPLoop
includes three loops, for which the contracts check that the return value is bigger than a given constant.
Pine.*
in Table 1). Listing 5 shows the nonlinear Pine.pendulumapprox
benchmark and the loop invariant that Pine has generated. This benchmark simulates a simple pendulum and uses a Taylor approximation of the sine function. The condition of the while loop is a placeholder for any condition, meaning that we are proving the loop invariant regardless of how many iterations the loop takes. We thus specify diverges true, which means that the method is (unconditionally) allowed to not terminate.Benchmark  # Goals  CVC4  Z3  MathSAT  

# Goals proven  Avg.  Max.  # Goals proven  Avg.  Max.  # Goals proven  Avg.  Max.  
Ex2  12  9(CE)  5.2  34.4  9(CE)  27.6  TO  9(CE)  3.4  22.7 
Ex2reset  16  16  0.8  4.2  16  19.3  162.8  16  0.9  2.9 
Ex3resetleadlag  15  15  0.7  5.7  15  0.4  496.8  15  0.9  8.5 
Ex7dampened  10  10  1.5  10.2  10  1.9  3081.0  10  3.9  34.2 
Filtergoubault  8  8  2.1  13.2  8  8.7  360.4  8  3.3  21.8 
Filtermine1  10  10  1.2  4.6  10  1.3  522.2  10  1.9  8.1 
Filtermine2  8  8  8.4  63.0  8  0.3  997.5  8  21.0  163.1 
Filtermine2nondet  8  8  0.9  2.7  8  14.1  707.7  8  0.8  3.6 
Harmonic  9  9  2.9  20.1  9  28.5  2643.0  9  2.7  20.2 
Pendulumapprox  10  10  47.2  223.7  9  4.9  TO  10  16.8  421.2 
Pendulumsmall  10  10  1.9  14.5  10  7.5  2412.5  10  1.8  14.6 
Symplectic  9  9  1.7  9.2  9  32.9  1989.1  9  3.4  21.5 
Summary  113  113  6.5  223.7  112  13.5  TO  113  5.0  421.2 
Ex2
in Table 6), because the semantics of Pine and KeY differ subtly. In Pine, the generated invariant and bounds are considered to be realvalued, whereas in KeY they are evaluated under a floatingpoint semantics. Rectangle
benchmark with quantified axioms in the SMT translationsversion  Applied change  # Goals  CVC4  Z3  

# Goals validated  Avg.  Max.  # Goals validated  Avg.  Max.  
v0  None (original)  32  31  2.3  TO  7  46.2  TO 
v1  Fewer classes (2) in v0  32  32  2.5  4.8  9  42.7  TO 
v2  Fewer classes (1) in v0  32  32  2.4  4.2  7  85.2  TO 
v3  Complicated intervals for all vars in v2  32  32  2.5  5.5  6  59.3  TO 
v4  Simpler math in v2  16  16  1.0  1.3  12  35.3  TO 
v5  Shorter interval for arg2 in v3  32  30  2.3  TO  9  95.1  TO 
v6  Longer interval for arg2 in v2  32  32  2.6  7.4  7  14.8  TO 
v7  Complicated interval for arg2 in v2  32  31  2.4  TO  7  23.9  TO 
v8  Shorter interval for arg2 in v0  32  32  2.5  4.2  7  46.5  TO 
Rectangle.scale
benchmark to assess the solver’s sensitivity to various changes, applied to the benchmark’s contract or its implementation.
v0: is the original version of the benchmark (Listing 1 using the second contract) and our baseline;

v1: reduces the number of classes involved to two, while keeping the same functionality;

v2: reduces the number of classes involved to one, while keeping the same functionality;

v3: modifies v2 such that variable bounds in the precondition become more “complicated” in terms of longer fractional parts (e.g., the bounds for
arg2
become [3.0000001, 6.4000000003] instead of [3.0001, 6.4000003]); 
v4: simplifies the mathematical expression of v2 (less arithmetic operations)

v5: modifies v3 such that
arg2
has a tighter bound, i.e., the interval width is smaller 
v6: modifies v2 such that
arg2
has a larger bound, i.e., the interval width is larger 
v7: modifies v2 such that only
arg2
has a “complicated” bound 
v8: modifies v0 such that
arg2
has a tighter bound
arg2
has a tighter bound. While Z3’s performance improves, CVC4 validates two goals less. On the other hand, increasing the bounds on arg2
does not seem to make a difference.arg2
is the bottleneck for this benchmark; when only arg2
has a “complicated” input interval, CVC4 proves less goals. Finally, constraining arg2
in the original benchmark more tightly allows CVC4 to validate all goals but Z3’s performance remains unaffected.arg2
in the original benchmark more tightly allows CVC4 to validate all goals (1 more). This behavior could be potentially exploited by, e.g., relaxing a variable’s bounds.4.4 Transcendental functions in KeY
Benchmark  # Goals  CVC4  Z3  MathSAT  

# Goals validated  Avg.  Max.  # Goals validated  Avg.  Max.  # Goals validated  Avg.  Max.  
Axioms in SMTLIB translation
 
Cartesian.toPolar  4  4  7.1  9.2  1  16.8  TO  –  –  – 
Polar.toCartesian  2  2  0.9  0.9  2  69.7  95.7  –  –  – 
Circuit.instantCurrent  2  1  123.6  TO  0  –  TO  –  –  – 
Circuit.instantVoltage  2  2  1.1  1.1  1  103.8  TO  –  –  – 
Summary  10  9  17.3  TO  4  65.0  TO  –  –  – 
Axioms as taclet rules in KeY with quantified formulas
 
Cartesian.toPolar  4  4  6.8  7.7  1  40.0  TO  –  –  – 
Polar.toCartesian  2  2  1.4  1.9  1  288.0  TO  –  –  – 
Circuit.instantCurrent  2  2  123.8  128.3  0  –  TO  –  –  – 
Circuit.instantVoltage  2  2  1.3  1.3  0  –  TO  –  –  – 
Summary  10  10  28.0  128.3  2  164.0  TO  –  –  – 
Axioms as taclet rules in KeY without quantified formulas
 
Cartesian.toPolar  4  4  6.9  7.5  1  23.5  TO  4  1.2  1.7 
Polar.toCartesian  2  2  1.5  2.3  2  52.6  81.2  2  0.6  0.8 
Circuit.instantCurrent  2  2  123.5  127.5  0  –  TO  0  –  TO 
Circuit.instantVoltage  2  2  1.5  1.7  2  146.4  160.7  2  0.8  0.8 
Summary  10  10  28.1  127.5  5  84.3  TO  8  1.5  TO 
sqrt
, comparing the approach from Sect. 3.2.2 (adding the necessary axioms, resp. taclet rules) to using the square root implemented in SMT solvers (fp.sqrt
). We chose to include only axioms specified in or inferred from the IEEE 754 standard. The set of used axioms are as follows:
If
arg
is NaN or less than zero, thensqrt(arg)
is NaN. 
If
arg
is positive infinity, thensqrt(arg)
is positive infinity. 
If
arg
is positive zero or negative zero, thensqrt(arg)
is the same asarg
. 
If
arg
is not NaN and greater than or equal to zero, thensqrt(arg)
is not NaN. 
If
arg
is not infinity and is greater than one thensqrt(arg)
<arg
.
Circuit.instantCurrent
benchmark which computes the instantanious current of an RL circuit (Listing 6), using the axiomatized square root, CVC4 is not able to validate the contract, but with fp.sqrt
the contract is validated. The reason our approach is unsuccessful on this benchmark is that the squareroot function appears early in the computation followed by atan and cos afterwards, resulting in complex expressions. In order to prove the corresponding proof obligations, in this case stronger axioms are needed.Benchmark  # Goals  CVC4  Z3  MathSAT  

# Goals validated  Avg.  Max.  # Goals validated  Avg.  Max.  # Goals validated  Avg.  Max.  
fp.sqrt  
Cartesian.toPolar  4  4  6.9  7.5  1  23.5  TO  4  1.2  1.7 
Cartesian.distanceTo  1  1  8.2  8.2  0  –  TO  1  1.0  1.0 
Circuit.instantCurrent  2  2  123.5  127.5  0  –  TO  0  –  TO 
Summary  7  7  40.4  127.5  1  23.5  TO  5  1.2  TO 
Axiomatized sqrt  
Cartesian.toPolar  4  4  2.0  2.9  4  49.81  163.0  4  1.0  1.6 
Cartesian.distanceTo  1  1  2.7  2.7  1  233.0  233.0  1  1.0  1.0 
Circuit.instantCurrent  2  0  –  TO  0  –  TO  0 (2 CE)  11.1  13.8 
Summary  7  5  2.1  TO  5  86.4  TO  5  3.9  13.8 
sqrt
axiomatically can result in shorter solving times than performing bitprecise reasoning, but the approach may not always succeed when the axioms are not sufficient to prove a particular property.4.5 Discussion and insights
sqrt
), we observed that handling these functions as uninterpreted with an appropriate axiomatization at the SMTLIB or the taclet level is a viable approach, with an interesting tradeoff between the verifier performance and the properties that can be proven. Clearly, properties that require exact semantics for transcendental functions will not be proven with our approach, but our experiments show that reasoning about the absence of special values is indeed possible. We further observe that both our approaches for adding axioms to the SMT queries or as taclet rules work to some extent, however, applying axioms as taclets in KeY directly has several advantages. Using taclets avoids quantified axioms in the SMT query, which in turn improves the performance. While the additional assertions do not compromise the theoretical decidability of the theory (since the quantified domains are finite), they add considerably to the complexity of the encoding for the bitblasting SATbased decision procedures such that running times may increase exponentially. The experiments have thus exposed a weakness of the SATbased verification approach: if symbols outside the canonical arithmetic operations with fixed semantics are used within a program or specification, providing semantics for these symbols within the SMTLIB translation is not efficient.5 Related work
float
and double
as uninterpreted sorts.