A validated real function calculus

Abstract : We present a framework for validated numerical computations with real functions. The framework is based on a formalisation of abstract data types for basic floating-point arithmetic, interval arithmetic and function models based on Banach algebra. As a concrete instantiation, we develop an elementary smooth function calculus approximated by sparse polynomial models. We demonstrate formal verification applied to validated calculus by a formalisation of basic arithmetic operations in a theorem prover. The ultimate aim is to develop a formalism powerful enough for reachability analysis of nonlinear hybrid systems.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-00641648
Contributor : Nathalie Revol <>
Submitted on : Wednesday, November 16, 2011 - 1:25:03 PM
Last modification on : Thursday, February 7, 2019 - 3:54:45 PM

Identifiers

  • HAL Id : hal-00641648, version 1

Collections

Citation

Pieter Collins, Milad Niqui, Nathalie Revol. A validated real function calculus. Mathematics in Computer Science, Springer, 2011, 5 (4), pp.437-467. ⟨hal-00641648⟩

Share

Metrics

Record views

266