PV4 PAF: Probabilistic Analysis of Floating-point computationscomputers sound but tight probabilistic bounds to roundoff errors in arithmetic expressions

Application domain/field

Expected input

Description of a probabilistic floating-point computation and its input distributions


Text file with own input format


Supports Z3 and dReal.


License: MIT
Floating point


Repository: https://github.com/soarlab/paf

Related papers

Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations (CAV '21)

Last publication date

15 July 2021

Related tools

Tools that focus on roundoff errors: FPTaylor, PrAn.

ProVerB specific

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