Animation of the autonomous chemical detector RoboChart model

Here we demonstrate the animation of an autonomous chemical detector using Interaction Trees in Isabelle/HOL.

The theoretical semantics is well-documented in this ICFEM2022 paper: “Formally Verified Animation for RoboChart Using Interaction Trees”.

The Isabelle/HOL theories for the animation can be found here.

This work is also presented at ICFEM2022 and the presentation can be found here.