A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1) , (1) , (2)
1
2
Pieter Collins
  • Function : Author
  • PersonId : 840906
Milad Niqui
  • Function : Author
  • PersonId : 868821
Nathalie Revol

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.
Fichier principal
Vignette du fichier
Collins-Niqui-Revol.pdf (88.16 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00473270 , version 1 (14-04-2010)

Identifiers

  • HAL Id : inria-00473270 , version 1

Cite

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⟩
173 View
162 Download

Share

Gmail Facebook Twitter LinkedIn More