## 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 language | English (US) |
---|---|

Title of host publication | Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Proceedings |

Editors | Omri Isac, Guy Katz, Radoslav Ivanov, Nina Narodytska, Laura Nenzi |

Publisher | Springer Science and Business Media Deutschland GmbH |

Pages | 147-163 |

Number of pages | 17 |

ISBN (Print) | 9783031212215 |

DOIs | |

State | Published - 2022 |

Event | 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 - Haifa, Israel Duration: Aug 11 2022 → Aug 11 2022 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 13466 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 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 |
---|---|

Country/Territory | Israel |

City | Haifa |

Period | 8/11/22 → 8/11/22 |

## All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)