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 metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/inria-00473270
Contributor : Nathalie Revol <>
Submitted on : Wednesday, April 14, 2010 - 7:49:44 PM
Last modification on : Thursday, February 7, 2019 - 2:21:00 PM
Long-term archiving on : Friday, October 19, 2012 - 2:01:42 PM

File

Collins-Niqui-Revol.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00473270, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

380

Files downloads

249