Advanced Software Analysis
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.
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.
- 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
Ordinary examExam type:
D: Submission of written work with following oral, External (7-point scale)
D1G: Submission for groups with following oral exam based on the submission. Shared responsibility for the report.