Dilian GUROV

Professor in Computer Science at 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 Univ. 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, ResearchGate 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

• iFM 2023 (PC member), TAP 2023 (PC member), TAP 2022 (PC member), ISoLA 2021 (Track co-organizer), iFM 2019 (PC member), GameSec 2019 (Local Arrangements Chair), FASE 2019 (PC member), ISoLA 2018 (Track co-organizer), FASE 2018 (PC member), PrePost 2017 (PC member), CSL 2017 (Workshops Chair), FASE 2017 (PC member), ISoLA 2016 (PC member and Track co-organizer), NWPT 2016 (PC member), iFM 2016 (PC member), VeCoDiS 2015 (a Lorentz workshop, co-organizer), FMSPLE 2015 (PC member), UaESMC 2014 (an ESORICS workshop, PC member), WING 2014 (PC member), FMSPLE 2013 (PC member), FoVeOOS 2011 (PC co-chair), ACM SAC 2010 (Software Verification and Testing track, PC member), FoVeOOS 2010 (PC member), PoFI 2010 (PC member),  SAVCBS 2009 (PC member)

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.
• AVerT2 (2022-2024) - Automated Verification and Test - Continuation, a Vinnova FFI collaborative project with Scania.

Past Projects

• 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: Akademi Ut).
  
• 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

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

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