Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Dilian Gurov
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,
Osquarsbacke 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
try out ProMoVer, our wrapper tool for procedure-modular verification
deductively: by means of proof
systems
program models and logics for compositional verification
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.
CVPP
(2001-) - an informal
collaborative project aiming at algorithmic verification of
control-flow properties of programs with procedures, with focus on
compositionality.
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.
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.
Dilian Gurov
Department of Theoretical Computer Science School of Computer Science and
Communications
KTH Royal Institute of Technology SE-100 44 Stockholm SWEDEN