Event Category: MSc Defence

OIL, short for Open Interaction Language, is a domain-specific language developed by Canon Production Printing B.V. It is a language that can be used for specifying, analyzing, and implementing models of system behavior. The tooling created for OIL can generate C++ code from OIL specifications. Part of this generated code is a scheduler that schedules …continue reading

Two optimizations for Zielonka’s recursive algorithm for solving parity games are investigated. The first optimization is partial re-decomposition, in which only the part of the graph containing vertices of SCCs which have 1 or more vertices removed will be re-decomposed. The second optimization is dynamic SCC maintenance, which builds an SCC tree for each SCC …continue reading

At Vitens, the biggest drinking water company from the Netherlands, most processes in extracting, purifying and delivering drinking water are automated using PLCs. In order to check PLC programs, translation schemes for the programming languages Function Block Diagram and Structured Text are defined into an SMT solver. Using the SMT solver, a set of typical …continue reading

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 that there exists a directed path between all nodes in the set. The normal implementation of Tarjan’s algorithm uses recursion. …continue reading

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