Search Results

Documents authored by Wolff, Burkhart

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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.7
An Operational Semantics in Isabelle/HOL-CSP

Authors: Benoît Ballenghien and Burkhart Wolff

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today a reference model for concurrency. In the fairly rich literature, several versions of operational semantics have been discussed, which should be consistent with the denotational one. This work is based on Isabelle/HOL-CSP 2.0, a shallow embedding of the failure-divergence model of denotational semantics proposed by Hoare, Roscoe and Brookes in the eighties. In several ways, HOL-CSP is actually an extension of the original setting in the sense that it admits higher-order processes and infinite alphabets. In this paper, we present a construction and formal equivalence proofs between operational CSP semantics and the underlying denotational failure-divergence semantics. The construction is based on a definition of the operational transition operator P ⇝e P’ basically via the After operator and the classical failure-divergence refinement. Several choices are discussed to formally derive the operational semantics leading to subtle differences. The derived operational semantics for symbolic Labelled Transition Systems (LTSs) can be potentially used for certifications of model-checker logs as well as combined proof techniques.
Cite as

Benoît Ballenghien and Burkhart Wolff. An Operational Semantics in Isabelle/HOL-CSP. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ballenghien_et_al:LIPIcs.ITP.2024.7,
  author =	{Ballenghien, Beno\^{i}t and Wolff, Burkhart},
  title =	{{An Operational Semantics in Isabelle/HOL-CSP}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.7},
  URN =		{urn:nbn:de:0030-drops-207355},
  doi =		{10.4230/LIPIcs.ITP.2024.7},
  annote =	{Keywords: Process-Algebra, Semantics, Concurrency, Computational Models, Theorem Proving, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.TIME.2020.15
TESL: A Model with Metric Time for Modeling and Simulation

Authors: Hai Nguyen Van, Frédéric Boulanger, and Burkhart Wolff

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract
Real-time and distributed systems are increasingly finding their way into critical embedded systems. On one side, computations need to be achieved within specific time constraints. On the other side, computations may be spread among various units which are not necessarily sharing a global clock. Our study is focused on a specification language - named TESL - used for coordinating concurrent models with timed constraints. We explore various questions related to time when modeling systems, and aim at showing that TESL can be introduced as a reasonable balance of expressiveness and decidability to tackle issues in complex systems. This paper introduces (1) an overview of the TESL language and its main properties (polychrony, stutter-invariance, coinduction for simulation), (2) extensions to the language and their applications.
Cite as

Hai Nguyen Van, Frédéric Boulanger, and Burkhart Wolff. TESL: A Model with Metric Time for Modeling and Simulation. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nguyenvan_et_al:LIPIcs.TIME.2020.15,
  author =	{Nguyen Van, Hai and Boulanger, Fr\'{e}d\'{e}ric and Wolff, Burkhart},
  title =	{{TESL: A Model with Metric Time for Modeling and Simulation}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.15},
  URN =		{urn:nbn:de:0030-drops-129837},
  doi =		{10.4230/LIPIcs.TIME.2020.15},
  annote =	{Keywords: Timed Systems, Semantics, Models, Simulation}
}
Document
DOI: 10.4230/DagRep.3.1.1
Symbolic Methods in Testing (Dagstuhl Seminar 13021)

Authors: Thierry Jéron, Margus Veanes, and Burkhart Wolff

Published in: Dagstuhl Reports, Volume 3, Issue 1 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13021 "Symbolic Methods in Testing". The aim of the seminar was to bring together leading researchers of this field; the seminary ended up with 38 participants from 10 countries: France, The Netherlands, The Unites States, Germany, Switzerland, United Kingdom, Brazil, Norway, Estonia and Italy. Through a series of presentations, discussions, and working group meetings, the seminar attempted to get a coherent picture of the field, which transcends the borders of applications and disciplines, of existing approaches and problems in formal testing. The seminar brought together, on the one hand, researchers from the different camps and various tools. The main outcome of the seminar is the exchange of information between different groups and the discussion of new trends (parallelization, cloud-computing).
Cite as

Thierry Jéron, Margus Veanes, and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). In Dagstuhl Reports, Volume 3, Issue 1, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{jeron_et_al:DagRep.3.1.1,
  author =	{J\'{e}ron, Thierry and Veanes, Margus and Wolff, Burkhart},
  title =	{{Symbolic Methods in Testing (Dagstuhl Seminar 13021)}},
  pages =	{1--29},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{1},
  editor =	{J\'{e}ron, Thierry and Veanes, Margus and Wolff, Burkhart},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.1.1},
  URN =		{urn:nbn:de:0030-drops-40060},
  doi =		{10.4230/DagRep.3.1.1},
  annote =	{Keywords: Automated Deduction, White-box testing, Black-box Testing, Fuzz-Testing, Unit-Testing,Theorem prover-based Testing}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact