PV2 Daisysynthesises a Scala or C program where performance of floating-point operations are optimised

Application domain/field

Type of tool

Performance optimizer

Expected input


Input file (one single file) should follow the structure:
  import daisy.lang._
  import Real._

  object TestObject {

    def function1(x: Real): Real \= {
      require(0 <= x && x <= 1)

      val z \= x + x
      z \* x

    } ensuring(res \=> res +/- 1e-5)

    def function2 ...
The repository has some more details

Expected output

Optimized program in Scala or C with the guaranteed error below the specified target error


Framework for verifying and optimizing numerical programs. Given a program it provides an efficient implementation for floating-point programs with elementary function calls. Uses Z3, dReal, MPFR, Metalibm
C Floating point Performance Scala Synthesis


Related papers

Sound Approximation of Programs with Elementary Functions (CAV '19)

Last publication date

12 July 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.