Dilian GUROV
Ph.D. from
Univ. of Victoria, Canada.
Associate Professor 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 5, room
4520.
Research Interests
My main interest is in program
correctness. I am investigating various approaches to formalizing and 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
suitable temporal
logics. I
investigate
algorithmic as well as deductive techniques.
My research focus lies on compositional verification:
- algorithmically:
combining maximal model
generation with model checking
- try out ProMoVer, our wrapper tool for procedure-modular verification
- deductively: by means of proof
systems
- program models and logics for compositional verification
General Presentations
Service
Projects
- UaESMC
(2012-2015) - a project supported by the 7th Framework Programme of the
EC within the FET (Future and Emerging Technologies) Open scheme.
- CVPP
(2001- ) - an informal
collaborative project aiming at algorithmic verification of
control-flow properties of programs with procedures, with focus on
compositionality.
Past Projects
- HATS (2009-2012) - an EU FET
project titelled Highly Adaptable and Trustworthy Software using Formal
Models.
- FoVeOOS (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.
- 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.
- 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
Science and Art
I am also interested in novel approaches to teaching that
challenge the established views on learning as a purely rational
activity and knowledge as a set of statements about objects. I'd like
to build a bridge with Art aiming to include the emotional aspects of
knowledge discovery and
learning.
Supervision
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