## 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*

## Anneke Huijsmans: Optimising parity game solvers using dynamic SCC maintenance

Two optimizations for Zielonka’s recursive algorithm for solving parity games are investigated. The first optimization is partial re-decomposition, in which only the part of the graph containing vertices of SCCs which have 1 or more vertices removed will be re-decomposed. The second optimization is dynamic SCC maintenance, which builds an SCC tree for each SCC *…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*

## Mark Bouwman: A formalisation of SysML state machines in mCRL2

My talk this Thursday will consist of three parts. (10 -15 min) I will practice my talk for FORTE, where I will present the paper “A formalisation of SysML state machines in mCRL2”. This paper reports on a formalisation of the semi-formal modelling language SysML in the formal language mCRL2. The formalisation focuses on a *…continue reading*

## Alexander Fedotov: McMillan’s algorithm for SAT-based unbounded model checking.

In this talk, I will discuss McMillan’s algorithm for fully SAT-based unbounded symbolic model checking. The method is based on computing Craig interpolants. In terms of performance, the algorithm is substantially more efficient than BDD-based model checking. I will also explain how we modify McMillan’s algorithm to analyze the backward reachability of initial states from *…continue reading*