Koen Degeling: New algorithms and heuristics for solving Variability Parity Games
Variability parity games are a recently proposed extension to well-known parity games that allow for verification of software product lines (SPLs). We propose new algorithms for solving variability parity games based on the existing priority promotion and SCC decomposition, and provide new heuristics for VPGs. We implemented these proposed algorithms, as well as an algorithm …continue reading
Tom Buskens: Optimizing the code generator for OIL
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
Anneke Huijsmans: Optimising parity game solvers using dynamic SCC maintenance
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
Jasper Stam: Formal verification of an industrial PLC program in Function Block Diagram and Structured Text
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
Geert van Ieperen: Visualisation of large Labelled Transition Systems
A formal model describes the behaviour of a program, protocol or other system. The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development. This thesis focuses on visualising such a state space …continue reading
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 that there exists a directed path between all nodes in the set. The normal implementation of Tarjan’s algorithm uses recursion. …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 the software architecture. Bram showed that it was possible to come up with a reasonable model that could even be …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 pertain to high-level language semantics or hardware program execution. This thesis focuses on verification of hardware memory model conformance, i.e. …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 are defined in terms of serial views using observations. We prove that any execution of a program by a multiprocessor satisfying this …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 of the largest PLC programs available at Tata steel have been written down, and their validity on the software has …continue reading