Reactive Programming

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.