Advanced Software Analysis
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).
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.
- 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 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.