Advanced Software Analysis (Autumn 2020)

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

Learning activities

We turn this course into a PC 2.0 course.  The outline for PC2.0 structure are: 
The teacher (in agreement with Head of Programme) choose another format for the teaching such as lectures, workshops or seminars, which is aligned with the intended learning outcome and the student population.
Learning activities of the PC 2.0 course form per definition also includes a written assignment with supervision.
The exam form for a PC 2.0 course is either C or D.
For this course the exam form remains D.

Please read more about the learning activities in the course room in LearnIT.

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.

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:
D2G: Submission for groups with following oral exam supplemented by the submission. Shared responsibility for the report.

Time and date