A validated real function calculus - Archive ouverte HAL Access content directly
Journal Articles Mathematics in Computer Science Year : 2011

A validated real function calculus

(1) , (2) , (3)
Pieter Collins
  • Function : Author
  • PersonId : 864607
Milad Niqui
  • Function : Author
  • PersonId : 868821
Nathalie Revol


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.
Not file

Dates and versions

hal-00641648 , version 1 (16-11-2011)


  • HAL Id : hal-00641648 , version 1


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


Gmail Facebook Twitter LinkedIn More