MSc in Computer Science - Specialization in Logic, Semantics and Verification
Aarhus, Denmark
DURATION
4 Semesters
LANGUAGES
English
PACE
Full time
APPLICATION DEADLINE
Request application deadline *
EARLIEST START DATE
Aug 2025
TUITION FEES
EUR 15,300 / per year **
STUDY FORMAT
On-Campus
* 15 January for non-EU citizens and 1 March for EU citizens
** for non-EU/EEA students only | EU/EEA students study for free
Introduction
Specializations in Computer Science
The master’s programme runs over two years with four semesters. Three semesters are dedicated to specialisations or electives. The last semester is for your master’s thesis, which some choose to write in collaboration with a company. Once enrolled, our programme manager will help you complete your master’s programme based on your interests.
Specialization
- Two 30 ECTS specializations
Elective
- The recommendation is a 3rd specialization.
- A small number of elective courses in computer science are offered in addition to specializations. Project work (partly) is also a possibility.
- Elective courses may be supportive rather than core computer science, e.g. extra mathematics courses.
- There may be requirements for the composition of the study program in connection with possible admission.
- In this case, mandatory courses replace elective courses (partly).
Thesis
- Written within the area of specialization 1 or 2.
Logic, Semantics and Verification Specialization*
1st Sem (Fall): Formal Software Verification (10 ECTS)
2nd Sem (Spring): Algorithmic Model Checking (10 ECTS)
3rd Sem (Fall): Program Logics (10 ECTS)
*Semesters are independent – and can be taken in any order
Admissions
Curriculum
Formal Software Verification
Course content
The course includes
- Theory and practice of interactive theorem proving.
- Reasoning about functional programs using a proof assistant.
- Theory of basic type systems such as simple type theory, and the calculus of constructions.
- Advanced functional programming techniques, for example: effects, type classes and property-based testing
The mandatory assignments are a combination of exercises in an interactive theorem prover, programming exercises and theoretical exercises.
Description of qualifications
After the course, the participants will understand key concepts in Formal Software Verification: interactive theorem proving, basic and dependent type systems, and reasoning about functional programs using a proof assistant. Participants will learn some advanced functional programming techniques in the process.
Algorithmic Model Checking
Course content
The fundamental question in model checking is “Does a system meet its intended behaviour?” The course is an introduction to the theory and practice of model checking.
The first step is to make the question precise: the course will introduce modelling formalisms of systems (e.g., transition systems, automata) and specification languages (e.g., Linear Temporal Logic) that express the intended behaviour. We will proceed with the algorithmic task of answering the model-checking question. Two general approaches will be explored, namely, explicit and implicit model checking. Explicit techniques will be based on automata and omega-regular languages, trace inclusion and bisimulation. Symbolic techniques will be based on Binary Decision Diagrams and SAT (satisfiability) solving. Afterwards, the course will take a deeper look into concurrency. We will formulate the main algorithmic principles for model checking, such as partial order reduction and bounded context switching, and introduce some basic concepts around runtime verification, whereby a concurrent program is checked for errors while it is running.
The course will conclude with some paper-presentation lectures, where students will choose a scientific paper out of a curated list of relevant topics to present.
Description of qualifications
Purpose
The purpose of the course is to introduce the students to the principles of automated model checking at two levels: (A) at the semantics level, concerned with the models and specification languages that are used to describe system correctness, and (B) at the algorithmic level, concerned with the algorithms that are used to analyze these models and their specifications.
Program Logics
Course content
This course gives an introduction to program logic for formal program verification. Program logics are powerful mathematical theories and techniques aimed at reasoning about complex properties of programs (e.g., functional correctness or security properties) that are often beyond the reach of automated techniques. In particular, modern program logic can be used to reason about programs with mutable shared data structures, higher-order functions, and concurrency, three programming language features which are very important in practice, but challenging to reason about. In this course, we will study such program logic and explore how we can use it to reason about the correctness properties of sophisticated concurrent programs.
Description of qualifications
Purpose
The participants will after the course know the basic principles of program logic for formal program verification.