A validated real function calculus

Pieter Collins, Milad Niqui, Nathalie Revol

Research output: Contribution to journalArticleAcademicpeer-review

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 languageEnglish
Pages (from-to)437-467
Number of pages31
JournalMathematics in Computer Science
Volume5
DOIs
Publication statusPublished - 2011

Cite this