• 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

• understanding of LTL and CTL model checking
• understanding of Markov models and probabilistic model checking
• practical experience of developing a probabilistic model checker
• practice in independently studying, analysing, and explaining recent research in probabilistic verification

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.

Model checking is a classic technique to verify that a system model satisfies a given set of formally stated requirements. Models can be represented as labelled transition systems (LTS); popular requirement languages are CTL and LTL. When systems are subject to stochastic effects, e.g. due to random faults or by using randomised algorithms, we need probabilistic modelling formalisms, probabilistic requirement languages, and probabilistic model checking algorithms. In this course, students learn the mathematical and computer science concepts behind classic and probabilistic model checking - LTS, CTL, LTL, Markov chains, Markov decision processes, probabilistic CTL, etc. - and apply them by implementing their own high-performance probabilistic model checker. Students conclude the course by studying and presenting recent scientific results in probabilistic verification.