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.
Original language | English |
---|---|
Pages (from-to) | 437-467 |
Number of pages | 31 |
Journal | Mathematics in Computer Science |
Volume | 5 |
DOIs | |
Publication status | Published - 2011 |