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