Benchmarks used in the paper Verifying Floating-Point Programs in Stainless by Andrea Gilot, Axel Bergström and Eva Darulova, TACAS 2026 (doi:10.1007/978-3-032-22749-2_1). An extended version of the paper is available as arXiv:2601.14059.
This set of benchmarks includes Scala translations of the KeY verifier's floating-point benchmarks, lemmas about a Scala translation of the FdLibm math library, and a set of real-world floating-point functions mined from GitHub.
If you use these benchmarks, please cite the paper:
Gilot, A., Bergström, A., Darulova, E. (2026). Verifying Floating-Point Programs in Stainless. In: Junges, S., Katz, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2026. Lecture Notes in Computer Science, vol 16506. Springer, Cham. https://doi.org/10.1007/978-3-032-22749-2_1
@inproceedings{gilot2026stainlessfp,
title = {Verifying Floating-Point Programs in Stainless},
author = {Gilot, Andrea and Bergstr{\"o}m, Axel and Darulova, Eva},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2026)},
series = {Lecture Notes in Computer Science},
volume = {16506},
pages = {3--22},
year = {2026},
publisher = {Springer Nature Switzerland},
doi = {10.1007/978-3-032-22749-2_1},
note = {Extended version: arXiv:2601.14059}
}A machine-readable citation is in CITATION.cff.
benchmarks/key/— 8 benchmarks translated from the KeY verifier's suitebenchmarks/fdlibm/— 18 FdLibm functions translated to Scalabenchmarks/empirical/— 82 files covering 54 benchmarks mined from GitHubLICENSES/— the full text of every licence that applies to something hereATTRIBUTION.md— per-benchmark licence, copyright holder and upstream originCITATION.cff— machine-readable citation for the paper
| Set | Benchmarks | Description |
|---|---|---|
benchmarks/key |
8 | Scala translations of the Java floating-point benchmarks used to evaluate the KeY verifier. |
benchmarks/fdlibm |
18 | Lemmas about an adaptation of the Java standard math library (java.lang.FdLibm). |
benchmarks/empirical |
82 files, 54 benchmarks | Floating-point functions mined from open-source Scala projects on GitHub, annotated by hand and grouped by verification outcome. |
Each benchmark in the empirical set is a Scala floating-point function extracted from a public GitHub repository, together with its dependencies, and annotated with a specification.
Benchmarks are grouped by what Stainless reports.
| Directory | Files | Meaning |
|---|---|---|
verified/ |
48 | Every verification condition is proved valid. |
counterexample/ |
19 | At least one VC is invalid and the counterexample is genuine: the code really can violate its contract. |
spurious_counterexample/ |
8 | A VC is reported invalid but the counterexample is not real. |
timeout/ |
3 | At least one VC exceeds the 300-second per-VC timeout used in the paper. |
unknown/ |
2 | At least one VC returns unknown. |
excluded/ |
2 | Break the tool rather than fail it: MetricCounter causes a stack overflow in termination inference, and Stainless loops forever on FPSLogger. |
A benchmark can appear in two directories at once. Where Stainless produced a genuine counterexample, the implementation was corrected by hand and verified again, so the suite keeps both versions.
Target functions are sampled from a larger dataset of floating-point files mined from GitHub. We then extracted the functions using Scyros, filtering for code under an open-source licence. We removed functions that did not perform any floating-point computation, functions calling external libraries, tests, and functions using language features Stainless does not support.
The file functions_scala_return_fp.csv contains the results of this screening. Its
code column holds the reason for exclusion:
| Label | Count | Meaning |
|---|---|---|
OK |
103 | Kept for use as benchmarks. |
TRIVIAL |
178 | Returns a floating-point value without performing any floating-point computation, such as a getter. |
EXT |
97 | Calls an external library, directly or indirectly. |
STD |
70 | Uses a language feature Stainless does not support, such as macros, concurrency or bounded polymorphism. |
TEST |
54 | Belongs to a test suite rather than to the source code of the repository. |
We then annotated the functions with contracts independently of one another and agreed on a common specification, keeping both versions where we disagreed.
The 103 remaining functions come from 41 repositories. Functions from the same source file, together with their dependencies, are grouped into one benchmark.
To run the benchmarks, you need Java 17 and Stainless v0.9.9.3 or later. A tutorial on Stainless covers installation in detail and is a good starting point if you have not used Stainless before.
Stainless prints a summary table with one row per verification condition, giving its
result, the solver that discharged it and how long it took. A benchmark in verified/
should report every VC valid; one in counterexample/ should report at least one
invalid along with the counterexample.
The following options are relevant to running the benchmarks.
| Option | Meaning |
|---|---|
--solvers=[SOLVER,...] |
SMT solvers to use as a portfolio, for example smt-z3,smt-cvc5,smt-bitwuzla. |
--timeout=N |
Per-verification-condition timeout, in seconds. |
--vc-cache=[true|false] |
Cache verification conditions. Default true; set false for timing runs. |
--strict-arithmetic=[true|false] |
Overflow, bounds in typecasts and NaN checks in comparisons. Default true. |
Empirical benchmarks. We recommend leaving --strict-arithmetic on, since these checks
are part of what the set is meant to exercise. Most benchmarks are self-contained:
cd benchmarks/empirical
stainless-dotty --vc-cache=false --solvers=smt-z3,smt-cvc5,smt-bitwuzla \
verified/AbsoluteError.scalaFifteen of the 82 import utils.Utils.*, a small library of helper lemmas and list
operations, and need utils.scala passed alongside them:
stainless-dotty --vc-cache=false --solvers=smt-z3,smt-cvc5,smt-bitwuzla \
verified/JaccardSimilarity.scala utils.scalaKeY and FdLibm benchmarks. Both sets expect --strict-arithmetic=false, as KeY does
not perform these checks, and they degrade performance on the numerically intensive FdLibm
lemmas:
stainless-dotty --strict-arithmetic=false benchmarks/key/Rectangle.scala
stainless-dotty --strict-arithmetic=false benchmarks/fdlibm/Acos.scalaThis repository comprises multiple components, licensed separately.
The collection is Apache-2.0. The selection and arrangement of the benchmarks, the
specifications we wrote, and the documentation and provenance metadata are released under
the Apache License 2.0, as given in
LICENSE.
The FdLibm benchmarks are GPL-2.0 with the Classpath exception. The files in
benchmarks/fdlibm are a Scala adaptation of the Java standard math library, whose
java.lang.FdLibm is Oracle's and is distributed with OpenJDK under
GPL-2.0-only with the
Classpath exception. They remain under those
terms.
The KeY benchmarks are CC-BY-4.0. The eight files in benchmarks/key are Scala
translations of Java benchmarks from the Benchmark Repository for Floating-Point Support
in KeY by Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt
(https://doi.org/10.5281/zenodo.6572961), and remain under that repository's
CC-BY-4.0 licence.
Each .scala file under benchmarks/empirical is third-party code and remains under
the licence of the project it was extracted from. Every one carries
SPDX-FileCopyrightText and SPDX-License-Identifier tags naming its copyright holder
and licence; ATTRIBUTION.md and
benchmarks.csv record the same information
together with the exact upstream origin, and LICENSES/ holds the full
licence texts.
| Licence | Files |
|---|---|
Apache-2.0 |
41 |
MIT |
18 |
GPL-3.0-only |
11 |
BSD-3-Clause |
4 |
GPL-3.0-or-later |
4 |
AGPL-3.0-or-later |
2 |
GPL-2.0-only |
2 |
The following 19 files are under copyleft licences and carry obligations beyond attribution if you redistribute them:
counterexample/FollowTargetRule.scala(GPL-3.0-only)counterexample/PredictionMetrics.scala(GPL-3.0-or-later)counterexample/StormDay.scala(AGPL-3.0-or-later)excluded/FPSLogger.scala(GPL-2.0-only)spurious_counterexample/ExponentialMutagen.scala(GPL-3.0-only)spurious_counterexample/PolynomialMutagen.scala(GPL-3.0-only)unknown/JaccardSimilarity.scala(GPL-3.0-or-later)verified/FollowTargetRule.scala(GPL-3.0-only)verified/JaccardSimilarity.scala(GPL-3.0-or-later)verified/Kitchen.scala(GPL-2.0-only)verified/Kmath_a0.scala(GPL-3.0-only)verified/Kmath_a1.scala(GPL-3.0-only)verified/PairwiseScorer.scala(GPL-3.0-only)verified/Player_a0.scala(GPL-3.0-only)verified/Player_a1.scala(GPL-3.0-only)verified/PredictionMetrics.scala(GPL-3.0-or-later)verified/RectangularBorder_a0.scala(GPL-3.0-only)verified/RectangularBorder_a1.scala(GPL-3.0-only)verified/StormDay.scala(AGPL-3.0-or-later)
For the GPL and AGPL families we record -only unless the upstream project explicitly
says "or (at your option) any later version". See ATTRIBUTION.md for
the full per-benchmark table.
Every empirical benchmark is a modified version of its original. Functions were extracted from their surrounding code, adapted where necessary to the Scala subset Stainless supports, annotated with contracts, and in some cases corrected after a counterexample. The KeY benchmarks are likewise modified. They were translated from Java to Scala.
This statement is made to satisfy the change-notification requirements of Apache-2.0 section 4(b), of the GPL and AGPL, and of CC-BY-4.0. The modifications are the work of the benchmark authors and should not be attributed to the original authors, nor should these benchmarks be taken as representative of the upstream projects they were drawn from.
- The paper. Verifying Floating-Point Programs in Stainless, TACAS 2026: https://doi.org/10.1007/978-3-032-22749-2_1
- Extended version. https://arxiv.org/abs/2601.14059
- Paper artefact. Scripts and data for reproducing the paper's tables and figures: https://doi.org/10.5281/zenodo.18310707
- Stainless. The verifier these benchmarks target: https://github.com/epfl-lara/stainless
- KeY floating-point benchmark repository. The Java benchmarks the
keyset was translated from: https://doi.org/10.5281/zenodo.6572961 - Function dataset. The corpus of floating-point files mined from GitHub: https://doi.org/10.5281/zenodo.17055622
- Scyros. The framework used to extract the functions: https://github.com/fxpl/scyros