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
Lois Nijland: Adding sequential composition and termination to the linear time – branching time spectrum
Van Glabbeek presented the linear time – branching time spectrum of behavioural semantics and gave sound, ground-complete axiomatisations for the process theory BCCSP. Groote and Chen et al. proved for the semantics in the spectrum …continue reading
Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination
An alternative semantics for sequential composition in a setting with intermediate termination was proposed in a recent article by Baeten, Luttik and Yang. We consider two open questions regarding sequential processes with intermediate termination that …continue reading