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.
Type de document :
Article dans une revue
Mathematics in Computer Science, Springer, 2011, 5 (4), pp.437-467
Liste complète des métadonnées

Contributeur : Nathalie Revol <>
Soumis le : mercredi 16 novembre 2011 - 13:25:03
Dernière modification le : jeudi 7 février 2019 - 15:54:45


  • 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〉



Consultations de la notice