A verified ODE solver and the Lorenz attractor

DOI10.1007/s10817-017-9448-yzbMath1448.68460OpenAlexW2792892743WikidataQ90699726 ScholiaQ90699726MaRDI QIDQ1663218

Fabian Immler

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9448-y

zbMATH Keywords

ordinary differential equationPoincaré mapLorenz attractorrigorous numericsIsabelle/HOL

Mathematics Subject Classification ID

Nonlinear ordinary differential equations and systems (34A34) Numerical methods for initial value problems involving ordinary differential equations (65L05) Strange attractors, chaotic dynamics of systems with hyperbolic behavior (37D45) Algorithms with automatic result verification (65G20) Software, source code, etc. for problems pertaining to ordinary differential equations (34-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

The art of solving a large number of non-stiff, low-dimensional ordinary differential equation systems on GPUs and CPUs ⋮ Saddle-type blow-up solutions with computer-assisted proofs: validation and extraction of global nature ⋮ What is the point of computers? A question for pure mathematicians ⋮ Mathematics and the formal turn ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ A certificate-based approach to formally verified approximations ⋮ Verified interactive computation of definite integrals ⋮ Wild pseudohyperbolic attractor in a four-dimensional Lorenz system

Uses Software

• gmp
• Isabelle/HOL
• CakeML
• Autoref
• Transfer
• Lifting
• Refinement Monadic
• Archive Formal Proofs
• Dictionary Construction
• Affine Arithmetic
• Ordinary Differential Equations
• RODES

Cites Work

• Unnamed Item
• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Axioms and hulls
• Mathematical problems for the next century
• Isabelle/HOL. A proof assistant for higher-order logic
• A rigorous ODE solver and Smale's 14th problem
• The Lorenz equations: bifurcations, chaos, and strange attractors
• Affine arithmetic: concepts and applications
• The Flow of ODEs
• Formally Verified Approximations of Definite Integrals
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Verified Enclosure for the Lorenz Attractor (Rough Diamond)
• A compiled implementation of strong reduction
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
• Constructive Type Classes in Isabelle
• Singular hyperbolic systems
• The Lorenz attractor exists
• Refinement Calculus
• Deterministic Nonperiodic Flow
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The Picard Algorithm for Ordinary Differential Equations in Coq
• CakeML
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Automated Deduction in Geometry
• What's new on Lorenz strange attractors?