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

Pieter Collins (1) , Milad Niqui (1) , Nathalie Revol (2)

1 CWI - Centrum voor Wiskunde en Informatica
2 ARENAIRE - Computer arithmetic

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.

Mots clés: hybrid systems analysis; Taylor models; Coq

Domaines: Arithmétique des ordinateurs

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⟩