This repository contains the Isabelle Verification with Ordinary Differential Equations (IsaVODEs) tool. It is a tool for verifying hybrid systems in Isabelle/HOL, and is a collaboration between Jonathan Julián Huerta y Munive, Simon Foster and others. The tool provides an implementation of various techniques for reasoning about hybrid programs and differential equations, including André Platzer's differential induction technique, and also the use of flows and solutions.
In order to use this tool, you currently need Isabelle2025, the Ordinary Differential Equations AFP entry, and a set of components from our other repositories. The dependencies you need include:
- Optics,
mainbranch - Shallow Expressions,
mainbranch - Hybrid Library,
mainbranch - Z_Toolkit,
mainbranch - CAS-Integration,
masterbranch
Make Isabelle aware of them either by editing your ROOTS file (in /Users/user_name/.isabelle/Isabelle2025/ROOTS), or by making them Isabelle components. Users may start Isabelle with the Hybrid-Verification heap image already built-in with isabelle jedit -R Framed_ODEs to make the start time quicker. Once done, you should be able to run the theories in this repository.
- Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL. In ArXiV 2021: https://arxiv.org/abs/2102.02679
- Hybrid systems verification with Isabelle/HOL: Simpler syntax, better models, faster proofs. In FM 2021: https://doi.org/10.1007/978-3-030-90870-6_20
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification. In SEFM 2020: https://doi.org/10.1007/978-3-030-58768-0_5
- Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. In RAMiCS 2020: https://doi.org/10.1007/978-3-030-43520-2_11
- Predicate transformer semantics for hybrid systems. In JAR, 2022: https://doi.org/10.1007/s10817-021-09607-x