After five years of PhD research I am finishing my thesis on algorithms for fast term rewriting. In this talk I will look back on the project, summarize the results, and list the open problems

In this talk, I will give the intuition and outline of how to prove our new data-autonomous programming language AuDaLa Turing Complete. While doing that, I shall also discuss relevant aspects of the semantics, including the basics, null-elements and commands.

When formally verifying the correctness of mutual exclusion algorithms it is often assumed that interaction with the shared registers (i.e., reads and writes) are atomic. For instance, it is well-known that the correctness of Peterson’s algorithm relies on the atomicity assumption. Already in 1986, however, Lamport argued that implementing atomic interaction with shared registers basically …continue reading

A classical theorem states that the set of languages given by a pushdown automaton coincides with the set of languages given by a context-free grammar. In a recent article, Bas Luttik and I proved the pendant of this theorem in a setting with interaction: the set of processes given by a pushdown automaton coincides with …continue reading

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