2026-08-26T02:47:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26984 2026-07-16T09:49:33Z ddc:004 open_access

Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL Yan, Fang Ballenghien, Benoît Foster, Simon Cavalcanti, Ana Baxter, James Wolff, Burkhart process algebra Isabelle/HOL automated proof methods deadlock freedom 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. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. 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. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fang Yan and Benoît Ballenghien and Simon Foster and Ana Cavalcanti and James Baxter and Burkhart Wolff 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.10 urn:nbn:de:0030-drops-269849 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.10 eng https://creativecommons.org/licenses/by/4.0/legalcode