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.
Type de document :
Communication dans un congrès
NSV-3: Third International Workshop on Numerical Software Verification., Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00473270
Contributeur : Nathalie Revol <>
Soumis le : mercredi 14 avril 2010 - 19:49:44
Dernière modification le : vendredi 20 avril 2018 - 15:44:23
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 14:01:42

Fichier

Collins-Niqui-Revol.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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., Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00473270〉

Partager

Métriques

Consultations de la notice

338

Téléchargements de fichiers

225