Dilian GUROV

Professor in Computer Science in the Department of Theoretical Computer Science (TCS) of the School of Electrical Engineering and Computer Science (EECS) of the Royal Institute of Technology (KTH) in Stockholm. Ph.D. from the University of Victoria, Canada.

My office is located at KTH Main Campus, Osquars backe 2, floor 5, room 4520.

Research Interests

• Software Specification and Verification:
  • Contracts for software development
  • Program models, logics and tools
  • Compositional and procedure-modular reasoning
• Multi-Agent Strategic Planning:
  • Multi-player games with imperfect information
  • Synthesis of knowledge-based strategies

Publications

• Own Profile
• DBLP Profile 
• Google Scholar Profile

General Presentations

• Modular Software Verification, invited talk at RTA-CSIT 2014
• Modular Verification of Temporal Safety Properties of Procedural Programs, invited tutorial at SEFM 2011
• Compositional Verification of Interaction Behaviour, Docent lecture, March 2007

Service

Projects

Ongoing Projects

• FormAI (2023- 2026) - Formally Verified AI-Generated Software, a Vinnova AI for Advanced Digitalisation collaborative project with Scania and AI Sweden. The goal of the project is to explore how to combine Generative AI and Formal Verification (in the learning loop) to generate correct code for safety-critical embedded automotive software.

Past Projects

• AVerT2 (2022-2024) - Automated Verification and Test - Continuation, a Vinnova FFI collaborative project with Scania.
• AVerT (2019-2021) - Automated Verification and Test, a Vinnova FFI collaborative project with Scania.
• REVaMP (2017-2019) - Round-trip Engineering and Variability Management Platform and Process, an ITEA-3 project.
• CVPP (2001- 2016) - an informal collaborative project aiming at algorithmic verification of control-flow properties of programs with procedures, with focus on compositionality.
• PlaTE (2016-2017) - Multi-Robot Planning under Temporal-Epistemic Goals, a Small Visionary Project funded by the CSC school of KTH. The goal of the project was to develop a decentralized framework for collaborative multi-robot planning based on knowledge exchange.
• AkUt (2015-2016) - a collaboration with Scania on Functional Verification of C programs. The project was within a KLOSS initiative to get academics out to industry (Swedish: AkademiUt).
• UaESMC (2012-2015) - a project supported by the 7th Framework Programme of the EC within the FET (Future and Emerging Technologies) Open scheme.
• 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 STREP 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

• DD2557 Program Semantics and Analysis (spring 2025, period 4)
• DD2373 Automata and Languages (spring 2026, period 4)
• DD2452 Formal Methods (autumn 2024, period 1)

Science and Art

• FiXeno (2012-2013) was a joint project between Teater Giljotin and myself from KTH, funded by the Swedish Foundation for Innovative Culture, and centered around the abstract mathematical concepts of iterative transformations and fixed points.
• Here are some pictures from an experimental lecture on Discrete Mathematics, which took place on 29 September 2010, and an official press release by KTH (both texts in Swedish).

Supervision

Postdoctoral fellows

• Predrag Filipovikj (from August 2019 till December 2020)

Doctoral students

• Gustav Ung (industrial, since April 2024)
• Jesper Amilon (since January 2022)
• Christian Lidström (defended March 2024)
• Pedro de Carvalho Gomes (defended December 2015)
• Siavash Soleimanifard (defended September 2014)
• Irem Aktug (defended October 2008)
  

Master's projects (Examensarbete)

• Formal Specification and Verification of Automotive Software (at Scania)
• Various topics related to Program Verification (at KTH)
• Various topics related to Multi-Agent Games (at KTH)

Postal Address

Dilian Gurov
Department of Theoretical Computer Science
School of Electrical Engineering and Computer Science
KTH Royal Institute of Technology
Lindstedtsvägen 3
SE-100 44 Stockholm
SWEDEN

Tel: +46 8 790 81 98
Fax: +46 8 790 09 30
E-mail: dilian [at] kth.se