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 …continue reading

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? …continue reading

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 …continue reading

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 …continue reading

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 …continue reading

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 …continue reading

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 …continue reading

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 …continue reading