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:

• knowledge about program semantics to reason about program properties
• practical experience in developing tool support for static program verification
• understanding of the issues and solutions in encoding programs and program properties in an SMT solver
• knowledge about permission based separation logic to help reason about shared memory
• practical experience in using a state of the art static program verification tool
• understanding of the issues and solutions for verification of concurrent software with shared memory 

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.

This course familiarizes students with static program verification for imperative concurrent programs, by detailing the inner workings of program verifiers. At the end of the course, a student should understand how a program verifier is built and used. We introduce the use of SMT solvers to verify software. Concepts of static software verification are introduced by discussing how to build a program that generates SMT solvers in order to verify software. We also present how to define operational and axiomatic semantics of a program, and the relation between these two semantics. We discuss how verification is further complicated when dealing with a shared heap in concurrent software.