Skip to Main content Skip to Navigation
Journal articles

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 metadata
Contributor : Nathalie Revol Connect in order to contact the contributor
Submitted on : Wednesday, November 16, 2011 - 1:25:03 PM
Last modification on : Saturday, September 11, 2021 - 3:17:11 AM


  • HAL Id : hal-00641648, version 1



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



Record views