Skip to Main content Skip to Navigation
Conference papers

A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq

Pieter Collins 1 Milad Niqui 1 Nathalie Revol 2
2 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We present a framework for the verification of the numerical algorithms used in Ariadne, a tool for analysis of nonlinear hybrid system. In particular, in Ariadne, smooth functions are approximated by Taylor models based on sparse polynomials. We use the Coq theorem prover for developing Taylor models as sparse polynomials with floating-point coefficients. This development is based on the formalisation of an abstract data type of basic floating-point arithmetic . We show how to devise a type of continuous function models and thereby parametrise the framework with respect to the used approximation, which will allow us to plug in alternatives to Taylor models.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Nathalie Revol Connect in order to contact the contributor
Submitted on : Wednesday, April 14, 2010 - 7:49:44 PM
Last modification on : Saturday, September 11, 2021 - 3:17:34 AM
Long-term archiving on: : Friday, October 19, 2012 - 2:01:42 PM


Files produced by the author(s)


  • HAL Id : inria-00473270, version 1



Pieter Collins, Milad Niqui, Nathalie Revol. A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq. NSV-3: Third International Workshop on Numerical Software Verification., Fainekos, Georgios and Goubault, Eric and Putot, Sylvie, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00473270⟩



Record views


Files downloads