Exposés de recherche

Collection Exposés de recherche

00:00:00 / 00:00:00
168 380

Verified numerics for ODEs in Isabelle/HOL

By Fabian Immler

Also appears in collection : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certification

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.

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.18915703
  • Cite this video Immler, Fabian (14/01/2016). Verified numerics for ODEs in Isabelle/HOL. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.18915703
  • URL https://dx.doi.org/10.24350/CIRM.V.18915703

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
    community
  • Get notification updates
    for your favorite subjects
Give feedback