Advanced Software Analysis (Autumn 2019)

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

Advanced programming Modelling systems and languages

Intended learning outcomes

After the course, the student should be able to:

• Describe formally the meaning of a wide range of programming constructs
• Reason About semantic descriptions of programming languages
• Prove simple properties (structural induction)
• Analyze programs (program analysis)
• Discuss possibilities and limitations of automated static analysis
• Characterise some recent developments in programming languages and verification technology
• Mechanise and prove simple programs correct using the interactive proof assistant Coq

Learning activities

Mandatory activities

Ten individual weekly assignments. A student must pass eight of them. * If a student fails an assignment he/she will have one chance to submit in again the following week with the same deadline as the next assignment. If a student fails that assignment as well there will be no more opportunities submit in that particular assignment. * In order to be eligible for a second attempt the student must have made a serious attempt to submit the original assignment. Missing or incomplete assignments are not considered serious attempts. Later submissions are allowed only under very special circumstances. * There will be a mandatory lecture where the projects are presented in front of the class. Exemptions can be given in very special circumstances, but otherwise attendance and participation is mandatory.

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.

Ordinary exam

Exam type:
D: Submission of written work with following oral, external (7-trinsskala)
Exam variation:
D2G: Submission of written work for groups with following oral exam supplemented by the work submitted. The group has a shared responsibility for the content of the report.
Exam description:

Group exam type: Mixed exam 2

Maximum 3 students per group.

Project submission: Report + code.

Duration of exam: 35 minutes per student including voting. 

 The oral exam consist of a 5 minutes group presentation followed by a 30 minutes individual oral exam of each group member.

Time and date