User: Guest  Login
Original title:
A Verified ODE Solver and Smale's 14th Problem 
Translated title:
Ein Verifizierter GDGL-Löser und Smales 14. Problem 
Year:
2018 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Tucker, Warwick (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Theorem Prover, Isabelle, HOL, ODE, Rigorous Numerics, Lorenz Attractor 
TUM classification:
DAT 706d; DAT 540d 
Abstract:
This dissertation presents a formalization of ordinary differential equations (ODEs) and the verification of rigorous (with guaranteed error bounds) numerical algorithms in the interactive theorem prover Isabelle/HOL. The formalization comprises flow and Poincaré map of dynamical systems. The verified algorithms are based on Runge-Kutta methods and affine arithmetic. They certify numerical bounds for the Lorenz attractor and thereby lift the numerical part of Tucker's proof of Smale's 14th probl...    »
 
Translated abstract:
Diese Dissertation stellt eine Formalisierung von gewöhnlichen Differentialgleichungen (GDGL) und die Verifikation von rigorosen (mit garantierten Fehlerschranken) numerischen Algorithmen im interaktiven Theorembeweiser Isabelle/HOL vor. Die Formalisierung umfasst Fluss und Poincaré-Abbildung dynamischer Systeme. Die verifizierten Algorithmen basieren auf Runge-Kutta-Verfahren und affiner Arithmetik. Sie zertifizieren numerische Schranken für den Lorenz Attraktor und heben dadurch den numerische...    »
 
Oral examination:
09.05.2018 
File size:
22289865 bytes 
Pages:
161 
Last change:
12.07.2018