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

## Jan Martens: Resynchronizability of origin transducers

Origin semantics introduced by Bojańczyk is a fine grained semantics for transducers, that not only expresses the relation between input and output words, but also includes a function that given an output position returns the input position where it was produced: the origin. In this talk we’ll discuss resynchronizations, a tool to relax the notion *…continue reading*

## Ferry Timmers: Maintaining strongly connected components efficiently, under edge deletions

Assume we have a directed graph. We can find the strongly connected components in this graph using for instance Tarjan’s algorithm. Let’s say we remove an edge from the graph. Can we recalculate the SCCs? A (recent) paper by Bernstein, Probst et.al. presents a way tot do this efficiently. I’ll roughly discuss my experiences with *…continue reading*

## Mark Bouwman: Verification and model-based testing of a railway point/switch using mCRL2

The EULYNX initiative is a collaborative effort of more than ten European railway infrastructure managers to standardise signalling interfaces. Within EULYNX, FormaSig aims to use formal methods to analyse the correctness of the standard. We have recently concluded a case study in which we translate the EULYNX Point interface from SysML to mCRL2. The resulting *…continue reading*

## Tim Willemse: Family-Based SPL Model Checking Using Parity Games with Variability

We propose efficient family-based Software Product Lines (SPL) model checking based on variability parity games. These extend parity games with conditional edges labelled with (feature) configurations. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration *…continue reading*

## Thomas Neele: The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is *…continue reading*

## Tom Verhoeff: From FP to OO

This work got started while teaching a functional programming course, where I tried to make the abstract concept of F-(co-)algebras more concrete by stating that, in Java terms, these are just classes that implement a specific kind of generic interface. To make this even more concrete, I tried to implement this idea, together with the *…continue reading*

## Rob van Glabbeek: Is Speed-Independent Mutual Exclusion Implementable?

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker’s, Peterson’s and Lamport’s bakery are meant to be speed independent. In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending *…continue reading*

## Omar Alzuhaibi: Automata Learning with a Purpose

Abstract: In the field of automata learning, similar to model-based testing, a target machine is sent interrogative queries with the goal of uncovering its behaviour. The most common algorithm for this in the industry is L*_Mealy, a Mealy-machine-learning variant of Dana Angluin’s 1987 L*. In its current implementation, no means of filtering queries is available. *…continue reading*