## Jan Bergstra: From computability theory to computer science and back

I will discuss the sequence of themes which I have been researching since 1973, and try to highlight how research questions have come, and gone and reappeared. I will provide concise phrasings of leading principles *…continue reading*

## Jeroen Keiren: The basics of hardware verification using xMAS

xMAS is a graphical specification language that allows to describe hardware components such as communication fabrics by composing microarchitectural primitives such as queues. Hardware components described using xMAS are sufficiently precise to allow formal verification, *…continue reading*

## Rodin Aarssen: High-Fidelity Metaprogramming with Separator Syntax Trees

Many metaprogramming tasks, such as refactorings, automated bug fixing, or large-scale software renovation, require high-fidelity source code transformations – transformations which preserve comments and layout as much as possible. Abstract syntax trees (ASTs) typically abstract from *…continue reading*

## Wieger Wesselink: A Dafny proof of Tarjan’s strongly connected components algorithm

The mCRL2 toolset uses Tarjan’s strongly connected components algorithm at several places. To gain experience with automated provers, we have made a proof of this algorithm using Dafny, an automatic program verifier. In this talk I will explain *…continue reading*

## Rick Erkens: Abstraction for Bisimulation up to Context

Abstract: Roughly one year ago I gave a colloquium talk about up-to techniques for branching bisimilarity. In particular we discussed the soundness of branching bisimilarity up to context for CCS with guarded sums. In combination *…continue reading*

## Olav Bunte: Validity of OIL component specifications

With OIL one can model the desired behaviour of a system with a protocol specification and the actual behaviour of a component with a component specification. To choose what events to execute, an OIL component *…continue reading*

## Maurice Laveaux: Adaptive Non-linear Pattern Match Automata

Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of *…continue reading*

## Jan Friso Groote: Internally optimized decision diagrams

When trying to understand ZDDs, an alternative to BDDs, I was wondering whether a quite different view on representing boolean functions would be interesting. I called this different view Internally Optimized Decision Diagrams (IDDs). As it stands *…continue reading*

## Vincenzo Ciancia: Spatial Model Checking and Applications to Medical Image Analysis

Spatial aspects of computation are prominent in Computer Science, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However, formal verification techniques are usually concerned with temporal *…continue reading*

## Hans Zantema: Complexity of Automatic Sequences

Automatic sequences form an important class of infinite sequences: in some sense they describe the simplest pattern to obtain sequences that are not ultimately periodic. We give several equivalent definitions, and provide two natural ways to *…continue reading*