A Verified ODE Solver and the Lorenz Attractor

J. Autom. Reasoning, Volume 61, Issue 1-4, 2018, Pages 73-111.

Cited by: 13|Bibtex|Views2|
EI WOS
Other Links: dblp.uni-trier.de|link.springer.com|pubmed.ncbi.nlm.nih.gov|academic.microsoft.com
Keywords:
Isabelle/HOLLorenz attractorOrdinary differential equationPoincaré mapRigorous numerics

Abstract:

A rigorous numerical algorithm, formally verified with Isabelle/HOL, is used to certify the computations that Tucker used to prove chaos for the Lorenz attractor. The verification is based on a formalization of a diverse variety of mathematics and algorithms. Formalized mathematics include ordinary differential equations and Poincaré maps...More

Code:

Data:

Your rating :
0

 

Tags
Comments