Jordi van Laarhoven, MSc

Master Thesis

Graduation project at Canon Production Printing (Venlo, The Netherlands).

Seminar Formal System Analysis

Dr.ir. T.A.C. Willemse (Course Coordination)

Prof.dr.ir. J.F. Groote (Supervisor Research Project)

Winning Strategies in Quoridor: An analysis of the strategy game Quoridor. During this research project I investigated whether winning strategies exist in Quoridor. Using model checking, small instances of the game have been analyzed. We have strongly solved Quoridor for smaller instances of the game: The starting player has a winning strategy on a square board of even size and the opponent has a winning strategy on square boards of odd size.

• Quoridor
• Strongly Solved
• mCRL2
• Model Checking
• Formal Verification

System Validation

Prof.dr.ir. J.F. Groote

Applying formal techniques to improve the quality of software in (communicating) systems. The aim of the course is to learn how the behavior of systems can be modelled and how their behavior can be verified, using the mCRL2 Toolset and Language.

• mCRL2
• Axioms
• Abstract Data Types
• Process Equivalences
• Modal Mu-Calculus (with Data)
• Formal Proof Systems
• (Transformations to) Linear Processes
• Confluence (Reduction)

Process Algebra

Dr. S.P. Luttik

The course on Process algebra addresses the theoretical foundations of behavioural specification formalisms.

• Semantic Models of Behaviour
• Sequential Composition
• Parallel Composition
• Abstraction
• Recursion
• Structural Operational Semantics
• Behavioural Equivalences
• Congruence
• Equational Process Theories
• Soundness
• Completeness
• Elimination Theorem
• Fairness

Proving with Computer Assistence

Prof.dr. J.H. Geuvers

Proving with Computer Assistence addresses theorem provers ("proof assistants"). The course addresses how these theorem provers can be used to formalize programs to verify their correctness and discusses the type systems, both from the view of (functional) programming and logic, that form the theoretical basis for proof assistants like Coq.

• Theorem Provers
• Proof Assistants
• Coq
• Type Theory
• Dependent Type Theory
• Polymorphic Types
• Inductive Types
• Dependent Inductive Types
• Church-Rosser
• Normalization

Algorithms for Model Checking

Dr.ir. T.A.C. Willemse

The course Algorithms for Model Checking addresses the mu-calculus, CTL* and some of its subsets such as LTL and CTL, from a computational viewpoint. Mu-calculus model checking problems are transformed to frameworks of Boolean Equation Systems and Parity Games are addressed, combined with algorithm to solve these systems.

• CTL
• LTL
• Model Checking
• Fairness
• Modal Mu-Calculus
• Parity Games
• Small Progress Measures
• (Parametrised) Boolean Equation Systems

Automated Reasoning

Prof.dr. H. Zantema

Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.

• Satisfiability
• SAT Solving
• Resolution
• SMT
• Binary Decision Diagrams
• CTL
• Unification
• Reasoning Modulo Equations
• Term Rewriting
• Simplex Method
• Z3
• NUSMV

System Design Engineering

Dr.ir. I. Barosan

The course System Design Engineering addresses the significant aspects of Model-Based Systems Engineering (MBSE) including concepts, modeling and frameworks, based on ISO15288, ISO 42010. Complex models are modelled using System Design and Engineering Patterns.

• Model-Based Systems Engineering
• SysML
• Viewpoints
• Architecture
• TRIZ
• IBM Rhapsody
• System Modelling

Domain Specific Language Design

Dr.ir. L.G.W.A. Cleophas & dr. I. Kurtev

The course Domain Specific Language Design addresses the concepts needed for designing and developing domain specific languages.

• Rascal
• Eclipse Modeling Framework
• Lexical Analysis
• Context-Free Grammars
• Abstract Syntax
• Concrete Syntax
• Static Semantics
• Dynamic Semantics
• Code Generators
• Model Transformation Languages

Software Evolution

Dr. E. Constantinou

The course on Software Evolution addresses the challenges associated with software evolution. A set of methods and tools are discussed that address these challenges with their advantages and disadvantages. Furthermore, method and tools are aplied to existing software systems to analyze their evolution in a scientifically responsible way.

• Requirements
• Software Architecture
• Code Clones
• SourceCode Evolution
• Software Ecosystems
• Software Metrics
• Socal and Collaborative Software Development
• Threats
• Bugs
• Code Smells
• Refactoring
• Testing

Program Verification Techniques

Dr.ing. A.J. Wijs & dr. C. Huizing

The course Program Verification Techniques offers an introduction to the field of formal methods for the analysis of (models of) software systems, and provides the opportunity to get hands-on experience with formal verification tools.

• Correctness
• Formal Verification Techniques
• Symbolic Model Checkers
• Software Model Checkers
• Automatic Test Suite Generator
• Code Verifier
• LTL and CTL Model Checking
• Predicate Abstraction
• Abstraction-Refinement
• Assertional Verification
• Temporal Logic
• Propositional Logic
• First-Order Logic
• Hoare Logic

Advanced Algorithms

Prof.dr. M.T. de Berg

The course Advanced Algorithms addresses algorithmic problems that cannot effecienly be solved using traditional algorithmic tools and covers concepts and techniques to deal with such problems.

• Approximation Algorithms
• I/O-Efficient Algorithms
• Streaming Algorithms

Architecture of Distributed Systems

Dr. H. Mostafaei

The course Architecture of Distributed Systems addresses how distributed systems are described and designed. Core concepts of their architecture and internal communication mechanisms are provided, and various architectural design styles and ways these can be combined to obtain desired functionality and extra-functional properties are discussed.

• Architecture
• Architectural Styles
• View(point)s
• Interaction Styles
• Naming
• Blockchain
• Quality Attributes
• Fault Tolerance

Big Data Management

Dr. O. Papapetrou

The course Big Data Management addresses models of contemporary data intensive systems and their practical use. These models are: Parallel and distributed data processing (MapReduce, etc.), Data Stream Management Systems and Approximate Query Processing.

• Big Data
• MapReduce
• Hadoop
• Spark
• Synopsis

Engineering Data Systems

Dr. N. Yakovets

Insight into and knowledge of concepts, methods and techniques for the improvement of the performance of data-intensive systems and for the realization of characteristic database properties such as persistence, reliability and integrity.

• Data Statistics
• Sampling
• Storage and File Structure
• B-Trees
• Hashing
• Query Processing
• Query Planning
• Query Optimization
• Advanced Data Representation
• Indexing
• Acyclic Conjunctive Queries
• Worst-Case Optimal Join
• Transitive Closure

Cryptology

Prof.dr. T. Lange

Knowledge of all modern standard techniques (both symmetric as asymmetric) for the protection of data against unauthorized thirds. Also acquiring the mathematics that is necessary for the design of such systems and for the evaluation of their security.

• Public-Key Cryptography
• Symmetric-Key Cryptography
• Block Ciphers
• AES
• Stream Ciphers
• Hashing
• Message Authentication Codes
• Diffie-Hellman Key Exchange
• El Gamal
• Methods to compute Discrete Logarithms
• Index Calculus Method
• Elliptic Curves
• RSA
• Probabilistic Primality Tests
• Primality Proof
• Factorisation Algorithms

Principles of Data Protection

Prof.dr. S. Etalle & dr. N. Zannone

The course Principles of Data Protection addresses the most important access control models and privacy policies.

• Discretionary Access Control
• Mandatory Access Control
• Role-Based Access Control
• Role-Based Trust Management
• Attribute-Based Access Control
• Usage Control
• Privacy
• Privacy-aware Access Control
• eXtensible Access Control Markup Language (XACML)
• Reduction of Access Control Decisions

Foundations of Process Mining

Prof.dr.ir. B.F. van Dongen

The course Foundations of Process mining addresses the foundations of process mining. Three fundamental elements, namely processes, process models and event data are combined. The course discusses how process models can be made, analyzed and discovered, how event data can be pre-processed and how both data and models can be combined to analyze the processes they describe.

• Petri Nets
• Process Discovery
• Alpha Algorithm
• Language-based Region Theory
• Aligning Petri Nets
• Data Pre-processing
• Conformance CHecking
• Event Logs
• Fitness
• Precision
• Generalization
• Simplicity