Unconditional lowerbounds on run-time complexity are challenging. For instance, the best known lowerbound for CNF-SAT remains only linear, despite considerable research effort. Nevertheless, we consider NP-hardness a reliable indication that we should not search for a polynomial time algorithms. Having a similar framework indicating the intrinsic difficulty of problems within PTIME, such as linear, quadratic, …continue reading

This is joint work with Anton Golov (RU) Labelled transitions systems can be studied both in terms of modal logic and in terms of bisimulation. These two notions are connected by so-called Hennessy-Milner theorems, that show that states are bisimilar precisely when they satisfy the same formulas in some modal logic, in other words, when …continue reading

Complex abstract data types are often used to facilitate creating concise models of the behavior of realistic systems. However, static analysis techniques that aim to optimize such models often consider variables of complex types as a single indivisible unit. The use of complex data types thus negatively affects the optimizations that can be performed. To …continue reading

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

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

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

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

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

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

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