Official course description, subject to change:
Basic info last published 9/04-21

Advanced Software Analysis

Course info
ECTS points:
Course code:
Participants max:
Offered to guest students:
Offered to exchange students:
Offered as a single subject:
Price (single subject):
21250 DKK (incl. vat)
MSc. Master
MSc in Computer Science
Course manager
Associate Professor
Associate Professor, Head of study programme
Associate Professor, Head of study programme
Course semester
Efterår 2021
30 August 2021
31 December 2021

This course focuses on interactive and automated software analysis. It covers a wide range of skills required to develop tools that automatically analyse software (such as “Coverity” and Facebook’s “Infer code analysis tool) to using tools where you interactively prove correctness of programs (used by e.g. Microsoft, Intel, Google, and Amazon).


This course is the final course for the Software Analysis specialisation. It gets students as close as possible to the current research in the field.

We focus heavily on practical design and implementation. For the automated parts we will implement tools for automatic verification. This includes tools for analysing control flow and being able to detect bugs like possible null-pointer dereferencing or eliminating dead code. We will show how to do this in a scalable and modular way. For the interactive parts we will use and be aided by the interactive proof assistant Coq — nearly all proofs we do in this course will be aided by Coq which in effect means that all of your calculations will be checked for you, greatly reducing the risk of human error (it’s also incredibly addictive). These types of tools are used in industry and has, for instance, been used to prove the correctness of an optimising C-compiler and an SeL4 micro kernel.

Formal prerequisites
  • Experience with developing software;
  • Frustration with software developed by you or by other people; and
  • Curiosity on how to use software analyzers to make today's software more reliable
Intended learning outcomes

After the course, the student should be able to:

  • Describe the semantics of a wide range of programming constructs
  • Formally specify properties of programs using types or logics
  • Use established techniques for analysing programs
  • Discuss and characterise some recent developments in programming languages and verification technology
Ordinary exam
Exam type:
D: Submission of written work with following oral, External (7-point scale)
Exam variation:
D1G: Submission for groups with following oral exam based on the submission. Shared responsibility for the report.