Official course description:
Full info last published 24/05-22

Advanced Software Analysis

Course info
Language:
English
ECTS points:
15.0
Course code:
KSADSOA1KU
Participants max:
24
Offered to guest students:
yes
Offered to exchange students:
yes
Offered as a single subject:
yes
Price for EU/EEA citizens (Single Subject):
21250 DKK
Programme
Level:
MSc. Master
Programme:
MSc in Computer Science
Staff
Course manager
Associate Professor
Teacher
Full Professor
Teacher
Assistant Professor
Teacher
Associate Professor, Head of study programme
Teacher
Associate Professor, Head of study programme
Teacher
Assistant Professor
Course semester
Semester
Efterår 2022
Start
29 August 2022
End
31 January 2023
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 advanced type systems for safe programming. Both of these 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.

The course is split in three parts. The first part focuses on programming in the language Idris. Idris is a dependently typed functional programming language, which means that the type system can express properties of programs. We will see how to use this for type driven development, a style of programming where the compiler is used as a tool to ensure correctness of programs. 

In the second part, we will discuss how we can safely program concurrent/distributed systems. Our main focus will be on session types, a specification language for distributed protocols. We will use session types for verifying that communicating processes never reach communication errors or deadlocks. We will touch both theoretical and applied aspects: we will learn algorithms for checking code correctness and study implementations of session types in mainstream programming languages. 

In the third part of the course, we focus on three topics in intelligent methods for testing and fixing programs: synthesis of test data using satisfiability solving (satisfiability-modulo-theory), synthesis of high-coverage test data using symbolic execution, and automatic program repair (generating patches). We investigate the operating principles of these tools and learn to use them on case study programs.


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:

  • Use and discuss advanced type systems for safe software development
  • Formally specify properties of programs and data using types and logics
  • Use techniques for analysing and repairing programs
  • Discuss and characterise some recent developments in programming languages and verification technology
  • Use techniques for automatic generation of high-quality test data for programs
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, 5 Jan 2023, 08:00 - 14:00
Ordinary Exam Thu, 26 Jan 2023, 09:00 - 21:00
Ordinary Exam Fri, 27 Jan 2023, 09:00 - 21:00
Reexam - submission Wed, 22 Feb 2023, 08:00 - 14:00
Reexam - submission Tue, 21 Mar 2023, 09:00 - 12:00