IsaVODEs is a tool for modelling and verifying cyber-physical systems based on Isabelle/HOL. Its core notation combines discrete programming operators with ordinary differential equations (ODEs), to allow modelling of both software and the physical environment. IsaVODEs particularly benefits from Isabelle’s proof automation, and its implementation of multivariate analysis in the HOL-Analysis package, which provides support for vectors and matrices. In particular, IsaVODEs support verification of non-linear systems through symbolic reasoning.

This tutorial will teach participants how IsaVODEs can be applied to modelling and verification. We will introduce the basics of Isabelle/HOL, and then show how we can automate modelling and verification of imperative programs using Hoare logic. Following this, we will show how dynamics can be modelled using ordinary differential equations, and verify a number of examples, such as a thermostat and an aircraft collision avoidance algorithm, using techniques like differential induction and symbolic solutions to ODEs.

The structure of the tutorial will be four sessions, each consisting of 45 minutes of lecture, followed by 45 minutes of practical. Participants should bring their own laptop to benefit from the practical sessions, and the tools will be made available beforehand.

Recent publication: https://doi.org/10.1007/s10817-024-09709-2

Website: https://isabelle-utp.york.ac.uk/