Information about the course can be found in
the first set of slides
The course has two parts:
- Specification and verification of security protocols.
- Static Analysis.
The first part will be taught by
In the course we will work mainly on the blackboard, but we will use in parallel
the following slides.
Seminars and Laboratory
- Dataflow Analysis
- Variable and Memory Space Analysis
- Abstarct Domains
- Domain interaction
At the seminar we will prove the theorems, lemmas and propositions presented at
the course and will also work out static analysis of specific programs.
At the lab you will need to implement and analyze simple C programs
using the following static analysis products.
- LLVM static analysis tools
- students can form teams of two
- two teams can not present the same project
- teams choose a project by filling a form that will be available online
- proposed projects are split into four categories A,B,C,D
A. Møller and M.I. Schwartzbach,
Static Program Analysis,
Department of Computer Science, Aarhus, 2018.
[ HTML |
Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer
[ HTML ]