The PVS development
`affine_arith`

, which will be included in the
next release of the NASA
PVS Library,
formalizes the theory of affine arithmetic for expressions
involving constants, variables, addition, subtraction, multiplication,
and the power operation on variables. This development
includes the proof-producing strategy `aff-numerical`

for evaluating multivariate
polynomials with variables in interval domains.

- Mariano Moscato, César Muñoz, and Andrew Smith,
*Affine Arithmetic and Applications to Real-Number Proving*, Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science, Vol. 9236, pp. 294-309, 2015. BibTeX Reference.