Jeroen Keiren: Model checking in the context of digital twins
A In the setting of digital twins, real world systems and virtual models are kept in sync. If the implementation and the models share a common source of truth, such as a low-code model, this allows for a very tight integration of the different aspects of digital twins. In a collaboration with, among others, Eindhoven …continue reading
Erik de Vink: In search of stability: a probabilistic composition of stable processes is stable
Axiomatization of branching bisimulation for distributions has been established in the setting of a process language with nondeterministic and probabilistic choice in earlier work. Key ingredient to the proof of completeness of the proposed theory is the notion of stability of processes and the property that every distribution can evolve, within the same equivalence class …continue reading
Clemens Dubslaff: A hybrid modeling approach for feature-oriented systems
In feature-oriented software development, software product lines are defined as families of systems where features encapsulate incremental or optional behaviors. There are mainly two different approaches for specifying feature-oriented systems: either annotative of compositional, i.e., either guarding code by presence conditions over features or specifying components for each feature along with a composition operation. Both …continue reading
Mark Bouwman: Algorithms for Cheaper LEGO
Besides the official LEGO sets there are many fan-created designs online. To build these custom designs you need to buy individual parts online. Concentrated on two larger platforms there are thousands of stores offering parts. An interesting optimisation problem arises: which distribution of parts over the stores is the cheapest, also considering shipping costs? In …continue reading
Olav Bunte: An evaluation of the Spoofax language workbench in an industrial context
Language workbenches have been developed to ease the implementation of Domain Specific Languages (DSLs), which are used often in industry for better productivity and communication among engineers. However, only very little literature exists that evaluates the use of a language workbench for an industrial context. In a work in progress journal paper we do exactly …continue reading
Ferry Timmers: Raking and the Self-deducing machine
Raking is a method with which we can extract the behavior from software systems by instrumenting its source code. A key element of this method is something I have dubbed the self-deducing machine. In this talk I will go into more detail about this concept, and how it can be used to extract a state …continue reading
Flip van Spaendonck: Verification of the busy-forbidden protocol using an extension of the cones and foci proof framework
In a previous colloquium, we presented a new and efficient readers-writer lock with no resource contention between readers, called the Busy-Forbidden Protocol. For its verification, specifications of its implementation and its less complex external behavior are provided. However, we are unable to prove the equivalence of these models for more than 7 concurrent threads using …continue reading
Jan Friso Groote: Real equation systems
The toolset heavily relies on boolean equation systems, which are the workhorse to solve modal formulas. Boolean equation systems only permit truth values as solutions for variables. It would be nice to also extract quantitative information using modal formulas, such as probabilities, durations, or yields. For this purpose it would be nice to have real …continue reading
Hans Zantema: Turtle figures of morphic sequences
In September I retired and as a present I received from you a great art object in stained glass. This was a particular instance of a turtle figure of a morphic sequence, as will be described in this talk. The main message is that a program consisting of only a few lines may create a …continue reading
Allan van Hulst: Kernels and small quasi-kernels in directed graphs (guest speaker)
In this talk I would like to discuss recent developments on the subject of kernels and quasi-kernels in directed graphs. A kernel is an independent set K in a directed graph such that every vertex is reachable in at most one step from K. A quasi-kernel is a weakening of the concept of a kernel. …continue reading