Dilian GUROV
Ph.D. from
Univ. of Victoria, Canada.
Docent at the Department of
Theoretical
Computer Science (TCS)
of the School of
Computer Science and Communications (CSC)
of the Royal Institute of Technology (KTH)
in Stockholm.
My office is located at KTH Main Campus,
Osquars backe 2, floor 4, room
4417.
Research Interests
My main interest is in program
correctness. I am investigating various approaches to proving
properties of the interaction
behaviour of programs, such as the correct sequencing of method
calls in Java-like programs, message passing in Erlang programs, or
handshake communications in CCS-like process calculi, expressed in a
suitable temporal
logic. I
investigate
algorithmic as well as deductive techniques.
My research focus lies on:
- compositional verification
- algorithmically:
combining maximal model
generation with model checking
- deductively: by means of proof
systems
- program models and logics for compositional verification
- property enforcement and
certification
- specifying security policies
with security automata
- specifying self-monitoring
for a given security policy
- automatic proof generation for self-monitoring programs
- state space representations
- modal transition systems
for capturing open systems
behaviour
Projects
- HATS (2009-2012) - an EU FET
project titelled Highly Adaptable and Trustworthy Software using Formal
Models.
- ContraST (2009-2011) - a
project funded by the Swedish Research Counsil
(VR) that aims at the development of a theoretical framework,
algorithms and tools for mobile code
security . In our
approach, mobile
code is equipped with a contract
consisting of an
abstract model of its security-relevant
behaviour, together with some form of evidence that the model is a
safe approximation of the actual behaviour. The code consumer can then
use
this contract to check whether the code,
once deployed and executed, will obey the consumer's security policies.
- FVOOS (2008-2012) - a COST Action titelled Formal
Verification of Object-Oriented Software, with the goal to co-ordinate
the development of
verification technology to achieve reach and power needed to assure
reliability of object-oriented programs on industrial scale.
- CVPP
- an informal
collaborative project aiming at algorithmic verification of
control-flow properties of programs with procedures, with focus on
compositionality.
Past Projects
- S3MS
(2006-2008) - an EU STEP project
with the objective of creating a framework and a technological solution
for the trusted deployment and execution of communicating mobile
applications in heterogeneous environments. The framework is based on
the notion of contract and
their enforcement by means of (in-lined) runtime monitors.
- SEFROS
(2003-2006) - a project funded by the Swedish Research Counsil
(VR) that aimed
at
techniques for formal reasoning about open
systems based on an
explicit state space representation.
- VerifiCard
(2001-2003)
- an EU project that aimed at providing verification techniques
for multi-applet smart card applications running on the JavaCard
platform.
- ErlVer (1997-2001) - a Swedish
collaborative project
which explored compositional verification of open distributed systems
written in the Erlang
programming language.
Teaching
Supervision
Service
General Presentations
Postal Address
Dilian Gurov
Department of Theoretical Computer Science
School of Computer Science and
Communications
KTH Royal Institute of Technology
SE-100 44 Stockholm
SWEDEN
Tel: +46 8 790 81 98
Fax: +46 8 790 09 30
E-mail: dilian [at] csc.kth.se
- Understand and invent analog electronic devices with Circuit
Fantasia, by Cyril Mechkov.
- Elissaveta Pancheva's home page