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
The following strategies are
implemented via computational reflection using a
verified generic branch and bound algorithm (see
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.
- 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.
- 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
identifies links that are outside
the NASA domain