Déposez votre fichier ici pour le déplacer vers cet enregistrement.
- 210 p.
ISBN 978-0-7923-7309-4
Localisation : Colloque 1er étage (SHEF)
analyse de données statistiques # classification # discrimination # applications industrielles # analyse numérique # graphique d'ordinateur # arithmétique finie # algorithmes matriciels # reconnaissance de formes # biologie neuronale
65-06 ; 65D18 ; 65G40 ; 62-07 ; 68U05 ; 62P30 ; 62H30 ; 65G30 ; 68T10 ; 65F30 ; 92C20
... Lire [+]
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
Research talks;Computer Science
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
... Lire [+]
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
- xvi; 255 p.
ISBN 978-0-521-10214-8
Encyclopedia of mathematics and its applications , 0037
Localisation : Collection 1er étage
intervalle # système d'éuqations non-linéaire # théorie de Perron-Frobenius # M-matrice # H-matrice
65G30 ; 65-02 ; 65F05 ; 65F10 ; 65H10
... Lire [+]
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
- xv; 699 p.
ISBN 978-0-521-76135-2
Encyclopedia of mathematics and its applications , 0133
Localisation : Collection 1er étage
architecture informatique # algorithme # base # résidu # système de nombres # arithmétique rationnelle
68M07 ; 65G30 ; 65-01 ; 68-01
... Lire [+]
Déposez votre fichier ici pour le déplacer vers cet enregistrement.
- v; 89 p.
ISBN 978-1-4704-4214-9
Memoirs of the American Mathematical Society , 1292
Localisation : Collection 1er étage
existence globale # surface quasi-géostrophique # incompressibilité # assitance par ordinateur
35Q35 ; 65G30 ; 76B03
... Lire [+]
