Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL

Author name not available (Why is that?)

Publication date: 4 February 2021

Abstract: The Isabelle/HOL proof assistant has a powerful library for continuous analysis, which provides the foundation for verification of hybrid systems. However, Isabelle lacks automated proof support for continuous artifacts, which means that verification is often manual. In contrast, Computer Algebra Systems (CAS), such as Mathematica and SageMath, contain a wealth of efficient algorithms for matrices, differential equations, and other related artifacts. Nevertheless, these algorithms are not verified, and thus their outputs cannot, of themselves, be trusted for use in a safety critical system. In this paper we integrate two CAS systems into Isabelle, with the aim of certifying symbolic solutions to ordinary differential equations. This supports a verification technique that is both automated and trustworthy.

Has companion code repository: https://github.com/ThomasHickman/Isabelle-CAS-Integration

This page was built for publication: Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6359860)