A Real-Blasting Extension of cvc5 for Reasoning About Floating-Point Arithmetic
No abstract available.
Related papers
- Deductive Verification of Floating-Point Java Programs in KeY TACAS 2021
- Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages OOPSLA 2026
- A Compiler for Sound Floating-Point Computations using Affine Arithmetic CGO 2022
- Automatic detection of floating-point exceptions POPL 2013
- Building Better Bit-Blasting for Floating-Point Problems TACAS 2019
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions CPP 2026
- A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs CAV 2025
- Finding root causes of floating point error PLDI 2018