Multi angle Verified numerics for ODEs in Isabelle/HOL
Auteurs : Immler, Fabian (Auteur de la Conférence)
CIRM (Editeur )
Loading the player...
Résumé : 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.Codes MSC :
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.
34-04 - Explicit machine computation and programs (not the theory of computation or programming)
34A12 - Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions
37D45 - strange attractors - chaotic dynamics
65G50 - Roundoff error
65L70 - Error bounds
68N15 - Programming languages
68Q60 - Specification and verification (program logics, model checking, etc.)
68T15 - Theorem proving (deduction, resolution, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65G30 - Interval and finite arithmetic
65Y04 - Algorithms for computer arithmetic, etc.
65G20 - Algorithms with automatic result verification