Event Category: MSc Defence

–

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 pertain to high-level language semantics or hardware program execution. This thesis focuses on verification of hardware memory model conformance, i.e. …continue reading

–

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 are defined in terms of serial views using observations. We prove that any execution of a program by a multiprocessor satisfying this …continue reading

–

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 of the largest PLC programs available at Tata steel have been written down, and their validity on the software has …continue reading

–

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, to Boolean equation systems and to parity games. The results of this research are mixed but we have discovered approaches …continue reading

–

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

–

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

–

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

–

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.

–

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