Verification of Circus Processes
Isabelle/UTP includes a theory of reactive designs which is used to create the semantic model for the Circus modelling language. Circus combines modelling of relational state with CSP-style concurrency, and can thus be used to model and verify reactive systems.
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure