## Interval Arithmetic

The PVS development `interval_arith`

, which is part of the NASA PVS Library,
formalizes the theory of interval arithmetic for a large set of
expressions including special real-valued function such as square
root, trigonometric functions, and logarithm and exponential functions.
The development includes proof-producing stragegies for reasoning about numerical
expressions.

### Strategies

The following strategies are
implemented via computational reflection using a
verified generic branch and bound algorithm (see
`structures/branch_and_bound.pvs`

).

`numerical`

: Estimate the minimum and maximum values of real-valued
expressions. The accuracy of the estimation can be specified by the user.
`interval`

: Check validity and satisfiability of
relational formulas of real-valued expressions.
- Examples: rational
expressions, real-valued expressions.

### Publications

- Anthony Narkawicz and César Muñoz,
*A Formally Verified Generic Branching Algorithm for Global
Optimization*, Proceedings of the Fifth Working Conference on
Verified Software: Theories, Tools and Experiments (VSTTE 2013),
Lecture Notes in Computer Science, Vol. 8164, pp. 326-343, 2014. BibTeX Reference.
- Marc Daumas, David Lester, and César Muñoz,
*Verified real number
calculations: A library for interval arithmetic*, IEEE Transactions on Computers,
Volume 58, Number 2, 2009. BibTeX Reference.
- César Muñoz and David Lester,
*Real Number Calculations and Theorem Proving*,
Lecture Notes in Computer Science, Volume 3603, 2005.
BibTeX Reference.
- Marc Daumas, Guillaume Melquiond, and César Muñoz,
*Guaranteed Proofs Using Interval Arithmetic*,
Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH-17), 2005. BibTeX
Reference.

The tag

identifies links that are outside
the NASA domain