## Herman Geuvers: Programming with Higher Inductive Types

A relatively recent extension to type theory is “homotopy type theory”. This provides a new view on types, where a type A is interpreted as a topological space, a term t of type A is interpreted as a point in the space and a proof of an equality, p : q=t is interpreted as a *…continue reading*

## Olav Bunte: Dynamic systems of communicating OIL components

In the previous presentation, I showed how we can model asynchronously communicating OIL components in mCRL2. Since then, we have added a “new” operator in OIL which enables users to create new instances of components dynamically. I show how we model the addition of this operator in mCRL2, which required significant changes. Also, I show *…continue reading*

## Yousra Hafidi: Verifying Cordis models using mCRL2: some challenges

Cordis models are industrial, UML like models. There are some semantical differences compared to standard UML. We verify Cordis models using a translation to mCRL2. In order to verify such models, we have to over several obstacles. In this talk, I will discuss three main challenges that we face so far: (1) the accurate translation *…continue reading*

## Anton Wijs: Memory Efficient State Space Exploration on GPUs for Concurrent State Machines with Data

GPUexplore is a tool that exploits the computational power of graphics processors to efficiently construct state spaces, and on-the-fly check safety and liveness properties. Its current main practical limitation, though, is related to its input language. The tool accepts networks of Labelled Transition Systems, which were initially useful to test whether state space could be *…continue reading*

## Jan Friso Groote: On the random structure of behavioural transition systems.

What is the structure of a transition system that represent the behaviour of processes? We assumed that it was just an ordinary random graph, but got odd results when predicting the sizes of state spaces generated by lps2lts. Viewing state spaces as parallel non-communicating random state spaces gave far better results. This also helps in *…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*

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