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

Application domain/field

• Roundoff errors
• Probabilistic floating-point computations
• Floating-point arithmetic

Expected input

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

Format:

Text file with own input format

Internals

Supports Z3 and dReal.

Comments

License: MIT