F Nous contacter


0

Documents  65G20 | enregistrements trouvés : 2

O
     

-A +A

Sélection courante (0) : Tout sélectionner / Tout déselectionner

P Q

This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are carried out for abstract algorithms, which are specified in terms of real numbers and sets. These abstract algorithms are automatically refined towards executable specifications based on lists, zonotopes, and software floating point numbers. Optimizations for low-dimensional, nonlinear dynamics allow for an application highlight: the computation of an accurate enclosure for the Lorenz attractor. This contributes to an important proof that originally relied on non-verified numerical computations.
This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are ...

68T15 ; 34-04 ; 34A12 ; 37D45 ; 65G20 ; 65G30 ; 65G50 ; 65L70 ; 68N15 ; 68Q60 ; 68N30 ; 65Y04

Nous confions à nos ordinateurs de nombreux calculs mais la machine a des limites due à son arithmétique dite à virgule flottante. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ont des limites vers l'infiniment petit et l'infiniment grand. Hors de ces bornes, l'ordinateur produit des valeurs spéciales souvent inattendues. La première partie de cet exposé montrera que l'ordinateur n'est pas infaillible ou plutôt que son utilisation est parfois abusive. La seconde partie consisitera en une utilisation judicieuse de l'arithmétique flottante de façon à récupérer les erreurs ou à garantir un calcul
presque juste, même dans les cas pathologiques.
Nous confions à nos ordinateurs de nombreux calculs mais la machine a des limites due à son arithmétique dite à virgule flottante. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ...

65G50 ; 68T15 ; 65G20 ; 68Q60 ; 65Y04

Nuage de mots clefs ici

Z