## Mark Frenken: Code Generation and Model-Based Testing in Context of OIL

OIL is a domain-specific language under development at OcĂ© for specifying, analysing, and implementing software components. OIL is to have IDE support, transformations to formal modelling languages for requirement verification, and code generation towards general-purpose languages such as C++. Model-based testing is an approach to test whether the behaviour of an implementation conforms to the *…continue reading*

## Sjef van Loo: Verifying SPLs using parity games expressing variability

SPL verification can be costly when all the software products of an SPL are verified independently. It is well known that parity games can be used to verify software products. We propose a generalization of parity games, named variability parity games (VPGs), that encode multiple parity games in a single game graph decorated with edge *…continue reading*

## Stan Roelofs: Automatically proving equality of infinite sequences

First order inductive theorem proving deals with proving new equations based on a given set of equations. More specifically, we are interested in proving that the axioms logically imply the goals. In this presentation I will discuss how we can automate these proofs by induction. The equations can either describe finite or infinite terms. In *…continue reading*

## Msc presentation Johri van Eerd

Johri van Eerd will present his master thesis research on Monday August 26 at 15:00 in Atlas 2.215. His presentation addresses the question on whether term rewriting on GPUs is competitive compared to term rewriting on CPUs.

## Kevin Nogarede: An approachable language for formal requirements

Formal system verification is a mathematical technique for establishing whether a process meets certain design requirements. Typically, such techniques require notation in academic languages which are difficult for engineers to write and interpret. We aim to develop a new DSL for formalizing requirements that dramatically lowers the barrier of entry by introducing notation and concepts *…continue reading*

## Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2

At Sioux, a model-driven development tool is created. It allows users to create a model and generate software for specific hardware platforms. For this tool, Sioux wants to incorporate model checking in order to improve the correctness and safety of software. To see whether model checking is viable for industrial models, we want to explore *…continue reading*

## Mark Bouwman: A model-based test platform for rail signalling systems

As technology progresses, newer, and more complex, solutions are employed to verify that rail signalling systems are safe. Formal methods provide ways to increase rigour in the verification process. This precision, accompanied by the ongoing increase of computational power of computers, also opens up ways to partially automate parts of the verification process. We present *…continue reading*

## Hong Zhang: Quality metrics for ASOME data models

At ASML the ASOME data modelling language has been defined. Many system designers are defining models in this language, and the question is whether there is an easy way to assess that these models are ok. This can be done using metrics. The question is which metrics are proper. In this MSc research various metrics *…continue reading*

## Ferry Timmers: A complete axiomatisation for probabilistic trace equivalence

In the thesis a complete axiomatisation is given for probabilistic trace equivalence for finite

processes. The axiomatisation is remarkably complex, which may explain that nobody formulated

such a complete axiomatisation yet.

## Lisette Sanchez: Learning software behavior through active automata learning with data

The topic of the thesis is find out whether the LS* learning algorithm, that can learn register automata with abstract data parameters from actual software is practically applicable in an industrial context. The algorithm can for instance learn a queue with limited size that stores arbitrary natural numbers. The conclusion is that indeed practical software *…continue reading*