A verified ODE solver and the Lorenz attractor
From MaRDI portal
(Redirected from Publication:1663218)
Strange attractors, chaotic dynamics of systems with hyperbolic behavior (37D45) Nonlinear ordinary differential equations and systems (34A34) Numerical methods for initial value problems involving ordinary differential equations (65L05) 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)
Recommendations
- A verified enclosure for the Lorenz attractor (rough diamond)
- A computer proof that the Lorenz equations have ``chaotic solutions
- A rigorous ODE solver and Smale's 14th problem
- Computer assisted proof of chaos in the Lorenz equations
- Chaos in the Lorenz equations: A computer assisted proof. Part II: Details
Cites work
- scientific article; zbMATH DE number 1245559 (Why is no real title available?)
- scientific article; zbMATH DE number 1863395 (Why is no real title available?)
- A compiled implementation of strong reduction
- A rigorous ODE solver and Smale's 14th problem
- A verified enclosure for the Lorenz attractor (rough diamond)
- Affine arithmetic: concepts and applications
- Automated Deduction in Geometry
- Automatic Data Refinement
- Axioms and hulls
- CakeML
- Constructive Type Classes in Isabelle
- Data refinement in Isabelle/HOL
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- Deterministic Nonperiodic Flow
- Formally verified approximations of definite integrals
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Mathematical problems for the next century
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Refinement Calculus
- Singular hyperbolic systems
- The Lorenz attractor exists
- The Lorenz equations: bifurcations, chaos, and strange attractors
- The Picard Algorithm for Ordinary Differential Equations in Coq
- The flow of ODEs
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- What's new on Lorenz strange attractors?
- Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
Cited in
(15)- Mathematics and the formal turn
- Formally-verified round-off error analysis of Runge-Kutta methods
- Saddle-type blow-up solutions with computer-assisted proofs: validation and extraction of global nature
- Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
- A certificate-based approach to formally verified approximations
- Computer-assisted proofs for finding the monodromy of Picard-Fuchs differential equations for a family of K3 toric hypersurfaces
- Verified interactive computation of definite integrals
- A verified enclosure for the Lorenz attractor (rough diamond)
- A Coq formalization of Taylor models and power series for solving ordinary differential equations
- Axiomatization of compact initial value problems: open properties
- Algorithm and abstraction in formal mathematics
- The art of solving a large number of non-stiff, low-dimensional ordinary differential equation systems on GPUs and CPUs
- Wild pseudohyperbolic attractor in a four-dimensional Lorenz system
- A rigorous ODE solver and Smale's 14th problem
- What is the point of computers? A question for pure mathematicians
Describes a project that uses
Uses Software
This page was built for publication: A verified ODE solver and the Lorenz attractor
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663218)
