Proposals for Master's projects (Examensarbete)
If you are interested in performing a Master's project (sv.
examensarbete)
in the area of Program Analysis and Verification,
please contact me at: dilian at csc.kth.se.
I am interested in supervising Master's projects on the
following topics:
Static analysis for security policies
The project investigates the problem of using Hoare logic based
specification and verification for proving that a Java program
satisfies a given security policy. The
outcome of the project will be an annotation method for a suitably
chosen tool such as ESC/Java2, together with an evaluation of the
method
on a case study.
Flowgraph extraction for verification of control flow properties
of programs
The project investigates the problem of extracting control flow graphs
of Java (bytecode) programs for the purpose of verification of control
flow properties. The main task will be to design a tool for the
extraction of control flow graphs in
a format suitable as input to previously developed tools for
compositional program verification based on maximal models and for
pushdown
automata model checking.
Other possible project topics
- Verification of programs with procedures based on pushdown
automata
- Compositional program verification based on maximal models
- Verification of peer-to-peer algorithms
- Extracting finite-state models of system behaviour through
black-box testing
Prospective Master's students are also invited to propose a project of
their own in the area of Program Analysis and Verification.
Last modified: 4
February 2009