HOL-CSP: A Comprehensive Process Theory for Semantics and Proc-Omata Reasoning
Thursday 18 December 2025 at 14h00
ENS Paris-Saclay, Room 1B26 and online
Abstract: CSP (Concurrent Sequential Processes) is a theory for concurrent computations and interaction. HOL-CSP is a conservative embedding of CSP into Higher-order logic (HOL); this gives rise to an environment that allows formal, machine-assisted proof of behaviour which is rich in data. A particular class of processes can be seen as symbolic automata whose finite instances can be treated by a model-checker. HOL-CSP is very
expressive and allows for representing finite automata and their infinite extensions as occurring for dense time, physical systems, and parameterized process architectures. The overall goal of this thesis is to combine finite automata-representations with infinite HOL-CSP which paves the way for combined proof--techniques where classical model-checking does not scale up. In particular, we combine classical automata-theory with a theory of architectural composition and ways to integrate model-checking approaches into deductive reasoning over processes.
The theory development has been done with the Isabelle/HOL proof assistant.
The defense will be in English.
Jury:
- Jim Woodcock (U York, Rapporteur)
- Stephan Merz.(U Nancy, Rapporteur)
- Laure Petrucci (U Paris-13)
- Pascal Poizat (U Nanterre)
- Regine Laleau (U Paris-Creteil)
- Frederic Boulanger (U Paris-Saclay)
- Mihaela Sighireanu (U Paris-Saclay)
PhD Supervisors:
- Burkhart Wolff
- Catherine Dubois