Official course description:
Full info last published 27/05-21

Advanced Software Analysis

Course info
Language:
English
ECTS points:
15.0
Course code:
KSADSOA1KU
Participants max:
15
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
Exam type
ordinær
Internal/External
ekstern censur
Grade Scale
7-trinsskala
Exam Language
GB
Abstract

This course aims at making students proficient in a wide range of skills required to develop tools that automatically analyse software and to use tools to prove correctness of software according to formal specifications. Both of these techniques are employed in modern software development to ensure software quality and security in the face of ever-increasing complexity.


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. In the first part, we learn how to 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.

In the second part, we will use advanced type systems to precisely specify the desired behaviour of programs. To prove that programs satisfy these specifications, we will use automated tools such as type checkers or semi-automated tools such as interactive theorem provers. The latter allows us to use specification languages that are too expressive to be fully automated and therefore require further input by the programmer.


Formal prerequisites

  • Having taken the course Modelling Languages and Systems.
  • Experience with developing software;

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
Learning activities

Two weekly teaching sessions for 9 weeks followed by a project on a topic chosen by the students. The meetings will be a combination of lectures, student presentations and exercises with a focus on student participation


Mandatory activities
None.

The student will receive the grade NA (not approved) at the ordinary exam, if the mandatory activities are not approved and the student will use an exam attempt.

Course literature

The course literature is published in the course page in LearnIT.

Student Activity Budget
Estimated distribution of learning activities for the typical student
  • Preparation for lectures and exercises: 15%
  • Lectures: 20%
  • Exercises: 20%
  • Assignments: 25%
  • Project work, supervision included: 10%
  • Other: 10%
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.
Exam submisson description:
Project submission: Report + code.
The oral exam consist of a 5 minutes group presentation followed by a 25 minutes individual oral exam of each group member.
Group submission:
Group and individual
  • Maximum 3 students per group.
Exam duration per student for the oral exam:
30 minutes
Group exam form:
Mixed exam 2 : Joint student presentation followed by an individual dialogue. The group makes their presentations together and afterwards the students participate in the dialogue individually while the rest of the group is outside the room.

Time and date
Ordinary Exam - submission Thu, 6 Jan 2022, 08:00 - 14:00
Ordinary Exam Fri, 21 Jan 2022, 09:00 - 21:00