Prof. Markus Roggenbach (Swansea University) will give a talk in the elite program’s special lecture series. The talk will take place virtually as an online meeting at 4PM on December 3rd 2020. The title of the talk is “Tools for CSP – Overview and perspectives”.
Taking the “Children & Candy Puzzle” (see below) as a master example, we discuss what the various tools for the process algebra CSP offer for modelling and verifying systems. Besides covering the standard instruments of simulation and model checking, we also discuss interactive theorem proving for CSP, as exemplified in our tool CSP-Prover.
Besides the power to analyze infinite state systems, the theorem proving approach offers the possibility for deeper reflections on CSP such as verifying the algebraic laws of the language, and proving meta results such as the completeness of axiomatic semantics.
Children & Candy Puzzle: “There are k children sitting in a circle. In the beginning, each child holds an even number of candies. The following step is repeated indefinitely: Every child passes half of her candies to the child on her left; any child who is left with an odd number of candies is given another candy from the teacher. Claim: Eventually, all children will hold the same number of candies.”
Markus Roggenbach is Professor of Computer Science at Swansea University, Wales, United Kingdom. He studied Computer Science in Braunschweig and Karlsruhe, did his PhD in Mannheim, and worked as a postdoc in Bremen. In
Swansea, he built up an active research group on the topic of “Processes and Data”.