TY - GEN
T1 - Verified Numerical Methods for Ordinary Differential Equations
AU - Kellison, Ariel E.
AU - Appel, Andrew W.
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85144820285&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85144820285&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-21222-2_9
DO - 10.1007/978-3-031-21222-2_9
M3 - Conference contribution
AN - SCOPUS:85144820285
SN - 9783031212215
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 147
EP - 163
BT - Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Proceedings
A2 - Isac, Omri
A2 - Katz, Guy
A2 - Ivanov, Radoslav
A2 - Narodytska, Nina
A2 - Nenzi, Laura
PB - Springer Science and Business Media Deutschland GmbH
T2 - 5th 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
Y2 - 11 August 2022 through 11 August 2022
ER -