Static Analysis
General Information
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
Ioana Leuștean.
Courses
In the course we will work mainly on the blackboard, but we will use in parallel
the following slides.
- Dataflow Analysis
- Variable and Memory Space Analysis
- Abstarct Domains
- Domain interaction
Seminars and Laboratory
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.
- Frama-C
- LLVM static analysis tools
- cflow
Projects
Rules:
- 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
Projects List
Bibliography
|
[1]
|
A. Møller and M.I. Schwartzbach,
Static Program Analysis,
Department of Computer Science, Aarhus, 2018.
[ HTML |
PDF ]
|
|
[2]
|
A. Simon,
Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer
Overflow Vulnerabilities,
Springer, 2010.
[ HTML ]
|
![[E-mail address]](images/email.png)