Wouter Schols: Verification of an iterative implementation of Tarjan’s algorithm for Strongly Connected Components using Dafny
Tarjan’s algorithm for strongly connected components is used in the mCRL2 toolset. This algorithm finds all strongly connected components or SCC in a directed graph. Here an SCC is a maximal set of nodes such …continue reading
Bram Hooimeijer: Model Inference for Legacy Software in Component-Based Architectures
Bram Hooimeijer did do his research for the master thesis at ASML. The question was whether it is possible to construct models for the behaviour of software out of a single trace using information about …continue reading
Nikita Golovliov: Verification of Multiprocessor System Memory Model
In a shared memory multiprocessor system, the memory model determines the outcome of read operations at any time, given a partial order of memory operations induced by processor-issued writes and reads. A memory model may …continue reading
Wessel Sinnema: Verifying memory consistency in mCRL2
We present a general method to verify an mCRL2 model of a multiprocessor with respect to memory consistency and prove the correctness of this method. Consequently, we present a way to reformulate most memory models that …continue reading
Sebastiaan Verhoek: SMT solver verification of ladder logic in a production environment (Tata Steel)
It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the input language for SMT solvers has been written. Subsequently, requirements on some …continue reading
Elbert van de Put: Ant Colony Optimization for Model Checking
Ant Colony Optimization is an optimization algorithm that is inspired by the foraging behavior of ants. In this thesis I have applied Ant Colony Optimization to problems that are generated from the model checking problem, …continue reading
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