Wouter Schols: Verification of an iterative implementation of Tarjan’s algorithm for Strongly Connected Components using Dafny
Tarjan’s algorithm for strongly connected components is used in the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal set of nodes such …continue reading
Anton Wijs: “Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion”
When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to …continue reading
Tim Willemse: On Recursive Algorithms for Solving Parity Games
Parity Games are infinite duration, two-player graph games. Such games play an important role in verification, satisfiability and synthesis. In recent years, several quasi-polynomial time algorithms for solving parity games have appeared. One of the …continue reading
Rick Erkens: “Bloom’s Cool Congruence Formats for Weak Behavioral Equivalences: Make Branching Bisimilarity a Congruence Again”
The field of process algebra provides a way to model (concurrent) processes algebraically. The syntax of a process calculus is described by an algebraic signature and the semantics is described by a set of operational …continue reading
Maurice Laveaux: Decompositional Minimisation of Monolithic Processes
Compositional minimisation can be an effective technique to reduce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form, each sequential process is replaced by an abstraction, …continue reading
Bas Luttik: Off-the-shelf automated analysis of liveness properties for just paths
The motivation for the research that I will discuss in my talk is a claim by van Glabbeek and Höfner that CCS-like process algebras are not powerful enough to establish correctness of Peterson’s algorithm, and, …continue reading
Jan Friso Groote: A symmetric protocol to establish service level agreements
We present a protocol designed using mCRL2 to negotiate the optimal service level by two parties. The problem is inspired by a similar problem at ASML where software had to be written to decide whether a “chuck swap” …continue reading
Bram Hooimeijer: Model Inference for Legacy Software in Component-Based Architectures
Bram Hooimeijer did do his research for the master thesis at ASML. The question was whether it is possible to construct models for the behaviour of software out of a single trace using information about …continue reading
Hans Zantema: Complexity of puzzles
For several puzzles (often from Japanese origin) the following can be investigated How to solve them, either by backtracking or by SAT/SMT? How to generate them? How to prove NP-completeness? Currently I supervise several students …continue reading
Jan Martens: A parallel algorithm for bisimulation partition refinement
The notion of strong bisimilarity on LTSs is an equivalence that expresses whether states have the same behavior. In their pioneering work Kanellakis and Smolka proposed a partition refinement algorithm that finds the coarsest partition …continue reading