Prof. Andrew Appel | Formally Verifed Numerical Methods скачать в хорошем качестве

Prof. Andrew Appel | Formally Verifed Numerical Methods

Speaker(s) Andrew Appel Princeton University Date 6 July 2022 – 09:30 to 10:30 Venue INI Seminar Room 1 Session Title Formally Verifed Numerical Methods Event [VS2W01] Vistas in Verified Software Abstract To formally and foundationally verify correctness and accuracy of numerical software, we take a layered, end-to-end approach: prove that the C program correctly implements a floating-point functional model, prove that this float model accurately approximates a real-valued discretized functional model; prove that the real-valued functional model finds sufficiently accurate solutions to the mathematical problem. (Discretized means, 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 quantitative accuracy bound for the final result. We demonstrate the method on an ordinary differential equation initial value problem (ODE IVP). Co-authors: names and affiliations: Ariel E. Kellison (Cornell)