Verified Numerical Methods for Ordinary Differential Equations

Ariel E. Kellison, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Ordinary differential equations (ODEs) are used to model the evolution of the state of a system over time. They are ubiquitous in the physical sciences and are often used in computational models with safety-critical applications. For critical computations, numerical solvers for ODEs that provide useful guarantees of their accuracy and correctness are required, but do not always exist in practice. In this work, we demonstrate how to use the Coq proof assistant to verify that a C program correctly and accurately finds the solution to an ODE initial value problem (IVP). Our verification framework is modular, and concisely disentangles the high-level mathematical properties expected of the system being modeled from the low-level behavior of a particular C program. Our approach relies on the construction of two simple functional models in Coq: a floating-point valued functional model for analyzing the intermediate-level behavior of the program, and a real-valued functional model for analyzing the high-level mathematical properties of the system being modeled by the IVP. Our final result is a proof that the floating-point solution returned by the C program is an accurate solution to the IVP, with a good quantitative bound. Our framework assumes only the operational semantics of C and of IEEE-754 floating point arithmetic.

Original languageEnglish (US)
Title of host publicationSoftware Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Proceedings
EditorsOmri Isac, Guy Katz, Radoslav Ivanov, Nina Narodytska, Laura Nenzi
PublisherSpringer Science and Business Media Deutschland GmbH
Pages147-163
Number of pages17
ISBN (Print)9783031212215
DOIs
StatePublished - 2022
Event5th International Workshop on Software Verification and Formal Methods for ML-Enables Autonomous Systems, FoMLAS 2022 and 15th International Workshop on Numerical Software Verification, NSV 2022 - Haifa, Israel
Duration: Aug 11 2022Aug 11 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13466 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Workshop on Software Verification and Formal Methods for ML-Enables Autonomous Systems, FoMLAS 2022 and 15th International Workshop on Numerical Software Verification, NSV 2022
Country/TerritoryIsrael
CityHaifa
Period8/11/228/11/22

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Verified Numerical Methods for Ordinary Differential Equations'. Together they form a unique fingerprint.

Cite this