In this presentation, we present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. This talk is a preview of a presentation we will deliver at ITP 2026.

Simon Foster is a Senior Lecturer (Associate Professor) at the University of York, and a member of the RoboStar Centre on Software Engineering for Robotics. His primary research applies theorem proving to formal verification and he leads the development of Isabelle/UTP, a practical theorem prover for heterogeneous systems. He has applied Isabelle/UTP to verification tools for autonomous and mobile robots, cyber-physical systems, process algebras, and reactive programs. He has worked on a variety of EU and EPSRC projects using diverse aspects of formal verification and assurance, and he teaches logic and formal proof to undergraduate students.