After successfully completing this course, the student:

• is able to research, understand, and apply recent scientific results in software science
• is able to answer software-related research questions on an appropriate level of abstraction

The student acquires:

• understanding of LTL, CTL and the mu-calculus
• understanding of how to do model checking and synthesis of transition systems with respect to these languages using automata and games
• practical experience of developing a CTL model checker using binary decision diagrams
• understanding of the basic concepts related to parity games and their relation to LTL, CTL and the mu calculus
• practical experience in developing a parity game solver

Software is everywhere, and our society is depending more and more on software working reliably and efficiently. To make it more reliable and efficient, we need to have a thorough understanding of the behavior of software systems, and how we can analyse and improve this behavior. This course gives insights in current research directions in the area of software systems, and how these new ideas can be used to improve software.
 
The goal of the course Software Science is to teach several topics related to active, on-going research in software engineering and formal methods. Each edition of the course consists of one topic of recent research, presented in lectures complemented with exercise or lab sessions to gain practical experiences with the material introduced during the lectures. Each topic comes with one or more individual homework/project assignments.
If one is interested in more than one topic, it is possible to follow the course a second time choosing a different topic. In this way, one can study 2 topics for 10 ECTS.
 
Two important topics in computer science are model checking of a transition system with respect to some specification written in a specification language, and the synthesis of a transition system or “controller” that implements a specification. Popular specification languages are CTL, LTL and the mu calculus. At the end of the course, students should be familiar with these specification languages and able to do model checking and synthesis using automata and games.
Parity games are a relatively simple form of two-player games on a graph where one player tries to prove a (typically temporal) property and the other player tries to refute this property. At the end of the course, students should understand how parity games are related to proving temporal properties (in LTL) and how a parity game solver is built. They will learn the concepts of attractor computation and tangles, among others. They will gain practical experience implementing a solver to prove LTL properties and synthesize controllers for LTL properties.