Legacy software is one of the most common struggles of the current software industry, being costly to maintain yet essential for the ongoing industrial process. This makes refactoring especially risky. The black-box reverse engineering technique we call model learning comes to aid. As pleasant in theory, as perilous in application it is however. This presentation …continue reading

To manage design complexity, high-level models are used to evaluate the functionality and performance of design solutions. There is a significant gap between these high-level models and the Register Transfer Level (RTL) implementations actually produced by designers. We address the challenge of bridging this gap, namely, relating abstract specifications to RTL implementations. An important feature …continue reading

One way to perform model checking of a model mu-calculus formula on a linear process is to transform the problem into a parity game. The solution to this parity game also provides an answer to the original model checking question. However, for infinite systems, such as real-time systems, the parity game corresponding to most non-trivial …continue reading

I will give a demo of the tool we are developing based on our research about formal analysis of micro-architectures. Going through examples I will illustrate the main modelling and verification features we currently have implemented. An interesting aspect is that we can model asynchronous systems. This part still requires some research and might generate …continue reading

SAT/SMT solving is a general technique for automatically finding solutions for a wide range of problems. In this talk some basics of the underlying techniques are presented. First we focus on SAT = satisfiability of pure propositional formulas. Next we see how the same techniques can be extended to SMT = satisfiability modulo theories, in …continue reading

The coexistence of ZigBee and WiFi networks is one of the topics which has been investigated both empirically and mathematically. The empirical studies often lack scalability since the networks considered are very small. The mathematical models on the other hand often focus on a stable network, ignoring he dynamic interactions of unstable systems. We provide …continue reading

Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to …continue reading

Robin Milner proposed a set of axioms for the Kleene star to capture bisimulation equivalence. It is an open question whether this (or any other) set of axioms is complete. I would like to take this opportunity to report on some progress which has been made regarding this problem: 1) It is sufficient to rewrite …continue reading

The Spoofax language workbench supports the creation of programming environments for software languages using high-level declarative meta-languages for the various aspects of language definition. In this talk, I will give a brief overview of the capabilities of Spoofax and then zoom in on its meta-language for the specification of type systems based on scope graphs …continue reading

In approximately 1993 Paul Klint and coworkers developed the ATerm library as a basic library to perform language transformations. The intention from the outside was that this library would be suitable for parallel processing, but this never materialised. Throughout the years several experiment have been done and a number of quite advanced lock and wait …continue reading