PolyPaver | Home

A numerical theorem prover
with support for verifying floating-point programs in SPARK/Ada.

Mini examples

Some statements that PolyPaver proves automatically in a few seconds or minutes:

$\left( \begin{array}{l} a \in [-10, 10]\\ b \in [-10, 10]\\ b > a + 0.1 \end{array} \right) \implies e^{a} - e^{b} > (b - a) e^{\frac{a+b}{2}}$

$\left( \begin{array}{l} x \in [0, 1]\\ y \in [0, 1]\\ \end{array} \right) \implies e^{x+y} - e^{x}\in [-0.01, 0.01] + \int_x^{x + y} e^t\,\mathrm{d}t$

$\left( \begin{array}{l} x \in [0.5, 2]\\ r \in [0, 3]\\ r \in [-x^2/4+x, x^2/4+1]\\ r = (0.5 \otimes (r \oplus x \oslash r))\\ \end{array} \right) \implies 0.5 \otimes (r \oplus x \oslash r) \in (1+4[-\varepsilon, \varepsilon])\sqrt{x}$

where $$\otimes, \oplus, \oslash$$ are single-precision floating-point operations and $$\varepsilon$$ is the corresponding floating-point epsilon.

Under the hood

• PolyPaver relies on a multi-variate correctly rounded function interval arithmetic
• It currently uses (a version of) the polynomial interval arithmetic from the AERN library

Origin

• PolyPaver was first developed by Jan Duracz and Michal Konečný during Jan’s PhD study under Michal’s supervision.
• The project has been sponsored by EPSRC and Altran Praxis.