A verified ODE solver and the Lorenz attractor
type: Item
instance of: scholarly article
title: A verified ODE solver and the Lorenz attractor
zbMATH Open document ID: 1448.68460
author: Fabian Immler
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 34-04
Mathematics Subject Classification ID: 34A34
Mathematics Subject Classification ID: 37D45
Mathematics Subject Classification ID: 65G20
Mathematics Subject Classification ID: 65L05
zbMATH DE Number: 6921413
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: ordinary differential equation
zbMATH Keywords: rigorous numerics
zbMATH Keywords: Poincaré map
zbMATH Keywords: Lorenz attractor
describes a project that uses: gmp
describes a project that uses: CakeML
describes a project that uses: Archive Formal Proofs
describes a project that uses: RODES
describes a project that uses: Transfer
describes a project that uses: Isabelle/HOL
describes a project that uses: Refinement Monadic
describes a project that uses: Autoref
describes a project that uses: Lifting
describes a project that uses: Dictionary Construction
describes a project that uses: Affine Arithmetic
describes a project that uses: Ordinary Differential Equations
MaRDI profile type: Publication
Wikidata QID: Q90699726
full work available at URL: s10817-017-9448-y
OpenAlex ID: W2792892743
cites work: Refinement Calculus
cites work: Wave equation numerical resolution: a comprehensive mechanized proof of a C program
cites work: Designing and proving correct a convex hull algorithm with hypermaps in Coq
cites work: Affine arithmetic: concepts and applications
cites work: Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
cites work: A compiled implementation of strong reduction
cites work: Data Refinement in Isabelle/HOL
cites work: Constructive Type Classes in Isabelle
cites work: Theorem Proving in Higher Order Logics
cites work: Q4790670
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Singular hyperbolic systems
cites work: Proving tight bounds on univariate expressions with elementary functions in Coq
cites work: A Verified Enclosure for the Lorenz Attractor (Rough Diamond)
cites work: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
cites work: The Flow of ODEs
cites work: Axioms and hulls
cites work: CakeML
cites work: Automatic Data Refinement
cites work: Deterministic Nonperiodic Flow
cites work: Formally Verified Approximations of Definite Integrals
cites work: The Picard Algorithm for Ordinary Differential Equations in Coq
cites work: Automated Deduction in Geometry
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4226356
cites work: Mathematical problems for the next century
cites work: The Lorenz equations: bifurcations, chaos, and strange attractors
cites work: The Lorenz attractor exists
cites work: A rigorous ODE solver and Smale's 14th problem
cites work: What's new on Lorenz strange attractors?
DOI: 10.1007/S10817-017-9448-Y
description: scientific article; zbMATH DE number 6921413