## Jos Baeten: Integration of automata theory and process theory

Since 2007, I have been working on a project to integrate automata theory and process theory. The motivation is to present students with a model of a computer in a basic course on the foundations of computer science, that relates more closely to computers as they know them. A recent result in this project is *…continue reading*

## Hans Zantema: The paint pot problem and common multiples in monoids

On a finite sequence of paint pots the following steps are allowed: * Swap two consecutive non-empty pots. * If the two neighbours of a non-empty pot are empty, then divide the paint in the middle pot over the two neighbours, after which these neighbours will be non-empty and the middle one will be empty. *…continue reading*

## Flip van Spaendonck: The Busy-Forbidden Protocol, an efficient shared-exclusive access lock

Mutual exclusion algorithms such as Peterson’s, make sure only a single thread can be present in the exclusive section at a given time. Similarly, a shared-exclusive lock also provides a shared section, in which any number of threads can be present, but only if no thread is present in the exclusive section. In this talk, *…continue reading*

## Rick Erkens: Regular tree languages and (dis)analogies with regular languages

Tree automata are a generalisation of finite automata over words. A tree automaton accepts a set of ranked ordered trees (terms if you will) just like a DFA accepts a set of words over an alphabet. Most interesting properties that regular languages enjoy, carry over to regular tree languages in some sense. I will present *…continue reading*

## Maurice Laveaux: On The Fly Solving for Symbolic Parity Games

In model checking we are interested in determining whether a property is satisfied for a given system. In particular, we want to know whether the property holds for the initial state of the system. We often see, especially while developing the model, that properties are already violated in relatively few steps from the initial state. *…continue reading*

## Yousra Hafidi: On starvation freedom property of Peterson’s mutual exclusion algorithm for more than 2 processes

It is well known that Peterson’s algorithm for two processes is starvation free. In this talk I study the generalization of Peterson’s algorithm to N>2 processes using tournament trees. In particular, I will show how, contrary to the two processes version, this algorithm is not starvation free if we do not make any fairness assumptions. *…continue reading*

## Herman Geuvers: “Computer Assisted Mathematical Proofs: using the computer to verify computers”

A “Proof Assistant” is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness. I will outline how Proof Assistants work, how they are used to verify mathematical proofs and computer systems. Verifying a proof with a *…continue reading*

## Olav Bunte: Asynchronously communicating OIL components

In this presentation we focus on how we envision OIL components to communicate with each other. We define the behaviour of communicating OIL components using a formalism found in literature, namely the FIFO system, and we show how this can be modelled in mCRL2. Also, we show some typical unwanted behaviour in asynchronous communication and *…continue reading*

## Jeroen Keiren: Understanding Mutual Exclusion Algorithms using mCRL2’s counterexamples

Last week, Myrthe Spronck discussed mutual exclusion algorithms when using safe registers. In this week’s talk, I will stick with the topic of mutual exclusion algorithms, but switch back to using atomic registers. I will introduce Dekker’s algorithm for mutual exclusion. According to Dijkstra, this is the first algorithm to solve mutual exclusion between two *…continue reading*

## Myrthe Spronck: Safe registers and Aravind’s BLRU algorithm in mCRL2

For my bachelor research project, supervised by Bas Luttik, I set out to verify Aravind’s bounded least recently used (BLRU) algorithm for mutual exclusion using mCRL2. An interesting property of Aravind’s algorithm is that it can ensure mutual exclusion even when the registers used are safe, rather than atomic. In order to verify this property, *…continue reading*