BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formally Verifed Numerical Methods - Andrew Appel (Princeton Unive
 rsity)
DTSTART:20220706T083000Z
DTEND:20220706T093000Z
UID:TALK175760@talks.cam.ac.uk
DESCRIPTION:To formally and foundationally verify correctness and accuracy
  of numerical software\, we take a layered\, end-to-end approach: prove th
 at the C program correctly implements a floating-point functional model\, 
 prove that this float model accurately approximates a real-valued discreti
 zed functional model\; prove that the real-valued functional model finds s
 ufficiently accurate solutions to the mathematical problem. (Discretized m
 eans\, e.g.\, finite time-steps or a finite spatial mesh.) We compose all 
 these proofs into a single main theorem in Coq\, stating an overall quanti
 tative accuracy bound for the final result. We demonstrate the method on a
 n ordinary differential equation initial value problem (ODE IVP).&nbsp\;\n
 Co-authors: names and affiliations: Ariel E. Kellison (Cornell)\n&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR