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

https://hal.inria.fr/hal-00641648
Contributeur : Nathalie Revol <>
Soumis le : mercredi 16 novembre 2011 - 13:25:03
Dernière modification le : samedi 21 avril 2018 - 01:27:21

Identifiants

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

Partager

Métriques

Consultations de la notice

204