BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:A Verified ODE Solver and Smale&\;#39\;s 14th P
roblem - Fabian Immler (Technische Universität Mün
chen)
DTSTART;TZID=Europe/London:20170706T134000
DTEND;TZID=Europe/London:20170706T142000
UID:TALK73471AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/73471
DESCRIPTION:Smale'\;s 14th Problem is a conjecture about ch
aos in a
particular dynamical system\, the Lore
nz attractor. The problem was solved by
Warwick
Tucker with a combination of regular analysis and
a computer-assisted
part. The computer-assiste
d part yields numerical bounds on solutions of the
Lorenz ODE\, which are required to certify cha
os.
In this talk\, I will present the curre
nt library of ODEs
and verified numerical metho
ds in Isabelle/HOL\, and how I use it for a formal
verification of the computer-assisted part of
Tucker'\;s proof.
LOCATION:Seminar Room 2\, Newton Institute
CONTACT:INI IT
END:VEVENT
END:VCALENDAR