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

Advanced Software Analysis

Course info
Language:
English
ECTS points:
15.0
Course code:
KSADSOA1KU
Participants max:
10
Offered to guest students:
yes
Offered to exchange students:
yes
Offered as a single subject:
yes
Price (single subject):
21250 DKK (incl. vat)
Programme
Level:
MSc. Master
Programme:
MSc in Computer Science
Staff
Course manager
Associate Professor
Teacher
Associate Professor, Head of study programme
Teacher
Associate Professor, Head of study programme
Course semester
Semester
Efterår 2021
Start
30 August 2021
End
31 December 2021
Exam
Abstract

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).

Description

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.