16:00-17:30

Guest lecture by Prof. Markus Roggenbach (Swansea University)

Prof. Markus Roggenbach (Swansea University) will give a talk in the elite program’s special lecture series. The talk will take place as an online meeting.

Title

Tools for CSP – Overview and perspectives

Abstract

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.”