A Verified ODE Solver and the Lorenz Attractor
J. Autom. Reasoning, Volume 61, Issue 1-4, 2018, Pages 73-111.
Isabelle/HOLLorenz attractorOrdinary differential equationPoincaré mapRigorous numerics
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
Full Text (Upload PDF)
PPT (Upload PPT)