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 …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 …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 …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 …continue reading
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 …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 …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 …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 …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 …continue reading