DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.10

Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL

Authors: Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

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.

Cite as

Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{yan_et_al:LIPIcs.ITP.2026.10,
  author =	{Yan, Fang and Ballenghien, Beno\^{i}t and Foster, Simon and Cavalcanti, Ana and Baxter, James and Wolff, Burkhart},
  title =	{{Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.10},
  URN =		{urn:nbn:de:0030-drops-269849},
  doi =		{10.4230/LIPIcs.ITP.2026.10},
  annote =	{Keywords: process algebra, Isabelle/HOL, automated proof methods, deadlock freedom}
}

Search Results

Documents authored by Baxter, James

Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message