Rick Erkens: Automaton-based Techniques for Optimized Term Rewriting
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
Tom Franken: AuDaLa Turing Completeness & Semantics
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.
Bas Luttik: Verifying mutual exclusion algorithms: dropping the atomicity assumption
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
Jos Baeten: Parallel Pushdown Automata and Commutative Context-Free Grammars in Bisimulation Semantics
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
Jan Martens: Using the Strong Exponential Time Hypothesis (SETH) to show the hardness of PTIME problems.
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
Herman Geuvers: Directed Hennessy-Milner theorems
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
Anna Stramaglia: Simplifying process parameters of unfolding algebraic data types
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
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