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 which I have made use of in successive stages, and how and why these have changed. Finally I will discuss …continue reading

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, however, the explicit state space of such components suffers from the state space explosion problem. Therefore, other verification techniques have …continue reading

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 such details, and hence would require pretty printing, destroying the original program layout. Concrete syntax trees (CSTs) preserve all layout information, …continue reading

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 our solution, and tell something about our experiences with Dafny. This is joint work with Kees Huizing.

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 with other up-to techniques this result allows for more feasible proofs when attempting to prove two CCS terms bisimilar. We added …continue reading

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 uses a scheduler with run-to-completion semantics. However, to avoid undesired behaviour concerning this scheduler, we need to put some validity …continue reading

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 the input term. Most of the existing automaton based techniques are restricted to linear patterns, where each variable occurs at …continue reading

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 it is in no way clear whether this alternative view would be beneficial to represent large boolean functions, especially because I …continue reading

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 properties and do not explicitly handle spatial information. Our work stems from the topological interpretation of modal logics, the so-called …continue reading

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 define the complexity of such sequences, based on sizes of corresponding automata. It turns out that between these two measures there …continue reading