Dilian Gurov's Publications

• DBLP Profile
• Google Scholar Profile

Multi-agent strategic planning

• Knowledge-Based Strategies for Multi-Agent Teams Playing Against Nature
  Dilian Gurov, Valentin Goranko, and Edvin Lundberg
  Artificial Intelligence, vol. 309, August 2022, DOI: 10.1016/j.artint.2022.103728

Contracts for software development

• An Expressive Trace Logic for Recursive Programs
  Dilian Gurov, and Reiner Hähnle
  In Proceedings of: FSCD'25
  LIPIcs, vol. 337, pp. 21:1–21:22, 2025
• Post-Hoc Formal Verification of Automotive Software with Informal Requirements: An Experience Report
  Gustav Ung, Jesper Amilon, Dilian Gurov, Christian Lidström, Mattias Nyberg, and Karl Palmskog
  In Proceedings of: RE'24
• An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
  Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, and Philipp Rümmer
  In book: Guide to Software Verification with Frama-C, 2024
• Trace-based Deductive Verification
  Richard Bubel, Dilian Gurov, Reiner Hähnle, and Marco Scaletta
  In Proceedings of: LPAR'23
  EPiC Series in Computing, vol. 94, pp. 73-95, 2023
• Contract Based Embedded Software Design
  Christian Lidström and Dilian Gurov
  In Proceedings of: TASE'23
  Lecture Notes in Computer Science, vol. 13931, pp. 77-94, 2023
• Principles of Contract Languages - Report from Dagstuhl Seminar 22451
  Dilian Gurov, Reiner Hähnle, Marieke Huisman, Giles Reger, and Christian Lidström
  In:  Dagstuhl Reports, 27 p, 2023
• Deductive Verification Based Abstraction for Software Model Checking
  Jesper Amilon, Christian Lidström and Dilian Gurov
  In Proceedings of: ISoLA'22
  Lecture Notes in Computer Science, vol. 13701, pp. 7-28, 2022
• Alice in Wineland: A Fairy Tale with Contracts
  Dilian Gurov, Christian Lidström, Philipp Rümmer
  In: Ahrendt W. et al. (eds) The Logic of Software. A Tasting Menu of Formal Methods
  Lecture Notes in Computer Science, vol. 13360, pp. 229-242, 2022
• An Abstract Contract Theory for Programs with Procedures
  Christian Lidström, and Dilian Gurov
  In Proceedings of: FASE'21
• Lecture Notes in Computer Science, vol. 12649, pp. 152-171, 2021 (full version)
  Formally Proving Compositionality in Industrial Systems with Informal Specifications
  Mattias Nyberg, Jonas Westman, and Dilian Gurov
  In Proceedings of: ISoLA'20
  Lecture Notes in Computer Science, vol. 12478, pp. 348-365, 2020
• Constraint-Based Contract Inference for Deductive Verification
  Anoud Alshnakat, Dilian Gurov, Christian Lidström, and Philipp Rümmer
  In: W. Ahrendt et al. (Eds.) Deductive Software Verification
  Lecture Notes in Computer Science, vol. 12345, pp. 149-176, 2020
• A Hoare Logic Contract Theory: An Exercise in Denotational Semantics
  Dilian Gurov, and Jonas Westman
  In: Müller P., Schaefer I. (eds) Principled Software Development
  Springer, Cham, pp. 119-127, 2018
  

Software verification

• Automatic Program Instrumentation for Automatic Verification
  Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, and Philipp Rümmer
  In Proceedings of: CAV'23
  Lecture Notes in Computer Science, vol. 13966, pp. 281-304, 2023
  Recipient of a CAV Distinguished Paper Award 2023
• Bounded Invariant Checking for Stateflow Programs
  Predrag Filipovikj, Gustav Ung, Dilian Gurov, and Mattias Nyberg
  In Proceedings of: FMAS'22, 15 pages, 2022 (full version)
• Dynamic Vulnarability Detection on Smart Contracts Using Machine Learning
  Mojtaba Eshghie, Cyrille Artho, and Dilian Gurov
  In Proceedings of: EASE'21
  ACM, pp. 305-312, 2021
• An Abstraction Technique for Verifying Shared-Memory Concurrency
  Wytse Oortwijn, Dilian Gurov, and Marieke Huisman
  Applied Sciences, vol. 10, no. 11, pp. 1-48, 2020
• Practical Abstractions for Automated Verification of Shared-Memory Concurrency
  Wytse Oortwijn, Dilian Gurov, and Marieke Huisman
  In Proceedings of: VMCAI'20
  Lecture Notes in Computer Science, vol. 11990, pp. 401-425, 2020
  
• Formal Verification in Automotive Industry: Enablers and Obstacles
  Mattias Nyberg, Dilian Gurov, Christian Lidström, Andreas Rasmusson, and Jonas Westman
  In Proceedings of: ISoLA'18
  Lecture Notes in Computer Science, vol. 11247, pp. 139-158, 2018
• Specification and Verification of Synchronization with Condition Variables
  Pedro de Carvalho Gomes, Dilian Gurov, Marieke Huisman, and Cyrille Artho
  Science of Computer Programming , vol. 163, pp. 174-189, 2018
• Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report
  Dilian Gurov, Christian Lidström, Mattias Nyberg, and Jonas Westman
  In Proceedings of: FMICS-AVOCS'17
  Lecture Notes in Computer Science, vol. 10471, pp. 3-18, 2017
• An Abstraction Technique for Describing Concurrent Program Behaviour
  Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, and Marina Zaharieva-Stojanovski
  In Proceedings of: VSTTE'17
  Lecture Notes in Computer Science, vol. 10712, pp. 191-209, 2017
• Formal Architecture Modeling of Sequential Non-recursive C Programs
  Jonas Westman, Mattias Nyberg, Joakim Gustavsson, and Dilian Gurov
  Science of Computer Programming, vol. 146, pp. 2-27, 2017
• Specification and Verification of Synchronization with Condition Variables
  Pedro de Carvalho Gomes, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FTSCS'16
  Communications in Computer and Information Science, vol. 694, pp. 3-19, 2017
• Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions
  Afshin Amighi, Pedro de Carvalho Gomes, Dilian Gurov, and Marieke Huisman
  Software Tools for Technology Transfer, vol. 18, no. 6, pp. 653-684, 2016
  Short version appeared in Proceedings of: SEFM'12
  Lecture Notes in Computer Science, vol. 7504, pp. 33-47, 2012
  
• Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs
  Pedro de Carvalho Gomes, Attilio Picoco, and Dilian Gurov
  In Proceedings of: FASE '14
  Lecture Notes in Computer Science, vol. 8411, pp. 215-229, 2014
• Program Models for Compositional Verification
  Marieke Huisman, Irem Aktug, and Dilian Gurov
  In Proceedings of: ICFEM'08
  Lecture Notes in Computer Science, vol. 5256, pp. 147-166, 2008

Logics of programs

• Soundness and Completeness of a Model-Checking Proof System for CTL
  Georg Friedrich Schuppe, and Dilian Gurov
  In: arXiv:2309.05389, 2023
• mu-Calculus with Explicit Points and Approximations
  Mads Dam, and Dilian Gurov
  Journal of Logic and Computation, vol. 12, no. 2, pp. 43-57, 2002
  (Abstract in Proceedings of: FICS 2000)
• A Note on Negative Tagging for Least Fixed-Point Formulae
  Dilian Gurov, and Bruce Kapron
  RAIRO Theoretical Informatics and Applications, vol. 33, pp. 383-392, 1999

Software product line modelling and verification

• Defining Categorical Reasoning of Numerical Feature Models with Feature-wise Quality Attributes
  Daniel-Jesus Munoz, Mónica Pinto, Dilian Gurov, and Lidia Fuentes
  In Proceedings of: SPLC'22, Volume B
  ACM, pp. 132-139, 2022
• Category Theory Framework for Variability Models with Non-Functional Requirements
  Daniel-Jesus Munoz, Dilian Gurov, Mónica Pinto, and Lidia Fuentes
  In Proceedings of: CAiSE'21
  Lecture Notes in Computer Science, vol. 12751, pp. 397-413, 2021
• Self-Correlation and Maximum Independence in Finite Relations
  Dilian Gurov, and Minko Markov
  In Proceedings of: FICS'15
  Electronic Proceedings in Theoretical Computer Science, vol. 191, pp. 60-74, 2015
• Model Mining and Efficient Verification of Software Product Lines
  Siavash Soleimanifard, Dilian Gurov, Ina Schaefer, Bjarte Østvold, and Minko Markov
  Serdica Journal of Computing, vol. 9, no. 1, pp. 35-82, 2015
• A Hierarchical Variability Model for Software Product Lines
  Dilian Gurov, Bjarte Østvold, and Ina Schaefer
  In Post-proceedings of: ISoLa'11
  Communications in Computer and Information Science, vol. 336, pp. 181-199, 2012
• Compositional Algorithmic Verification of Software Product Lines
  Ina Schaefer, Dilian Gurov, and Siavash Soleimanifard
  In Post-proceedings of: FMCO'10
  Lecture Notes in Computer Science, vol. 6957, pp. 184-203, 2011

Compositional verification of control flow-based safety properties

• Algorithmic Verification of Procedural Programs in the Presence of Code Variability
  Siavash Soleimanifard, and Dilian Gurov
  Science of Computer Programming, vol. 127, pp. 76-102, 2016
  Short version appeared in Proceedings of: FACS'14
  Lecture Notes in Computer Science, vol. 8997, pp. 327-345, 2015
  
• Procedure-Modular Specification and Verification of Temporal Safety Properties
  Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
  Software and Systems Modeling, vol. 14, no. 1, pp. 83-100, February 2015
  Short version appeared in Proceedings of: SEFM'11
  Lecture Notes in Computer Science, vol. 7041, pp. 366-381, 2011
• Reducing Behavioural to Structural Properties of Programs with Procedures
  Dilian Gurov, and Marieke Huisman
  Theoretical Computer Science, vol. 480, pp. 69-103, 2013
  Short version appeared in Proceedings of: VMCAI'09
  Lecture Notes in Computer Science, vol. 5403, pp. 136-150, 2009 (tool web-interface) (slides)
• CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties
  Marieke Huisman, and Dilian Gurov
  In Proceedings of: FoVeOOS'10
  Lecture Notes in Computer Science, vol. 6528, pp. 107-121, 2010
• Procedure-Modular Verification of Control Flow Safety Properties
  Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FTfJP'10, ACM Digital Library, 2010
• Compositional Verification of Sequential Programs with Procedures
  Dilian Gurov, Marieke Huisman, and Christoph Sprenger
  Journal of Information and Computation, vol. 206, no. 7, pp. 840-868, 2008
• Composing Modal Properties of Programs with Procedures
  Marieke Huisman, and Dilian Gurov
  In Proceedings of: FESCA'07
  Electronic Notes in Theoretical Computer Science, vol. 203, issue 7, pp. 87-101, 2009 (slides)
• Interface Abstraction for Compositional Verification
  Dilian Gurov, and Marieke Huisman
  In Proceedings of: SEFM'05
  IEEE Computer Society, pp. 414-423, 2005 (slides)
• Compositional Verification for Secure Loading of Smart Card Applets
  Christoph Sprenger, Dilian Gurov, and Marieke Huisman
  In Proceedings of: Memocode'04
  IEEE Formal Methods and Models for Co-Design, pp. 211-222, 2004
• Checking Absence of Illicit Applet Interactions: A Case Study
  Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov
  In Proceedings of: FASE'04
  Lecture Notes in Computer Science, vol. 2984, pp. 84-98
  Winner of the EASST award for Best Software Science Paper, 2004 (slides)
• Simulation Logic, Applets and Compositional Verification
  Christoph Sprenger, Dilian Gurov, and Marieke Huisman
  INRIA Technical Report RR-4890, 2003
• Temporal Logic and Toolset for Applet Verification:
  Compositional Reasoning, Model Checking, Abstract Interpretation
  Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa,
  Gennady Chugunov, Lars-Åke Fredlund, and Dilian Gurov
  VerifiCard Deliverable 4.1., 2002
• Model Checking of Multi-Applet JavaCard Applications
  Gennady Chugunov, Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: CARDIS'02
  USENIX Publications, pp. 87-95, 2002 (slides)
• Compositional Verification of Secure Applet Interactions
  Gilles Barthe, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FASE'02
  Lecture Notes in Computer Science, vol. 2306, pp. 15-32, 2002 (slides)
• Compositional Specification and Verification of Control Flow
  Based Security Properties of Multi-Application Programs
  Gilles Barthe, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FTfJP'01, 2001

Security and privacy

• Privacy Preserving Business Process Matching
  Dilian Gurov, Peeter Laud, and Roberto Guanciale
  In Proceedings of: PST'15, IEEE, pp. 36-43, 2015
• Business Process Engineering and Secure Multiparty Computation
  Roberto Guanciale, Dilian Gurov, and Peeter Laud
  In Ebook: Applications of Secure Multiparty Computation
  IOS Press, Chapter 7, pp. 129-149, 2015
• Privacy Preserving Business Process Fusion
  Roberto Guanciale and Dilian Gurov
  In Proceedings of: BPM-WS'14
  Lecture Notes in Business Information Processing, vol. 202, pp. 96-101, 2015
• Private Intersection of Regular Languages
  Roberto Guanciale, Dilian Gurov, and Peeter Laud
  In Proceedings of: PST'14, IEEE, pp. 112-120, 2014
• Provably Correct Runtime Monitoring
  Irem Aktug, Mads Dam, and Dilian Gurov
  Journal of Logic and Algebraic Programming, vol. 78, pp. 304-339, 2009
  Short version appeared in Proceedings of: FM'08
  Lecture Notes in Computer Science, vol. 5014, pp. 262-277, 2008 (slides)

State space representations for verification of open systems

• State Space Representation for Verification of Open Systems
  Irem Aktug, and Dilian Gurov
  In Proceedings of: AMAST'06
  Lecture Notes in Computer Science, vol. 4019, pp. 5-20, 2006
• Towards State Space Exploration Based Verification of Open Systems
  Irem Aktug, and Dilian Gurov
  In Proceedings of: AVIS'05
  Electronic Notes in Theoretical Computer Science, 2005

Verification of peer-to-peer algorithms

• Verification of Peer-to-peer Algorithms: A Case Study
  Rana Bakhshi, and Dilian Gurov
  In Proceedings of: MTCoord'06
  Electronic Notes in Theoretical Computer Science, vol. 181, pp. 35-47, 2007
• Verifying a Structured Peer-to-peer Overlay Network: The Static Case
  Johannes Borgström, Uwe Nestmann, Luc Onana Alima, and Dilian Gurov
  In Proceedings of: Global Computing'04
  Lecture Notes in Computer Science, vol. 3267, pp. 250-265, 2004

Compositional verification of behavioural properties of open distributed systems (Erlang, CCS)

• A Verification Tool for Erlang
  Lars-Åke Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, and Gennady Chugunov
  Software Tools for Technology Transfer, vol. 4, pp. 405-420, 2003
• Semi-Automated Verification of Erlang Code
  Lars-Åke Fredlund, Dilian Gurov, and Thomas Noll
  In Proceedings of: ASE'01
  IEEE Computer Society, pp. 319-323, 2001 (long version)
• The Erlang Verification Tool
  Thomas Noll, Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: TACAS'01
  Lecture Notes in Computer Science, vol. 2031, pp. 582-585, 2001 (slides)
• Verification of Erlang Programs: Factoring out the Side-effect-free Fragment
  Dilian Gurov, and Gennady Chugunov
  In Proceedings of: FMICS 2000
  GMD Report, no. 91, pp. 109-122, 2000
• A Framework for Formal Reasoning about Open Distributed Systems
  Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: ASIAN'99
  Lecture Notes in Computer Science, vol. 1742, pp. 87-100, 1999
• Compositional Verification of CCS Processes
  Mads Dam, and Dilian Gurov
  In Proceedings of: PSI'99
  Lecture Notes in Computer Science, vol. 1755, pp. 247-256, 2000
• System Description: Verification of Distributed Erlang Programs
  Thomas Arts, Mads Dam, Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: CADE'98
  Lecture Notes in Artificial Intelligence, vol. 1421, pp. 38-41, 1998
• Toward Parametric Verification of Open Distributed Systems
  Mads Dam, Lars-Åke Fredlund, and Dilian Gurov
  In book: Compositionality: The Significant Difference
  Lecture Notes in Computer Science, vol. 1536, pp. 150-185, 1998
• Specification and Verification of Communicating Systems with Value Passing
  Ph.D. Thesis, Department of Computer Science, University of Victoria, March 1998
• A Compositional Proof System for the Modal mu-calculus and CCS
  Sergey Berezin, and Dilian Gurov
  CMU Techreport CMU-CS-97-105, 1997
• A Modal mu-Calculus and a Proof System for Value Passing Processes
  Dilian Gurov, Sergey Berezin, and Bruce Kapron
  In Proceedings of: INFINITY'96
  Electronic Notes in Theoretical Computer Science, Vol.5, 1996

Other

• Formal Methods Research at SICS and KTH: An Overview
  Mads Dam, Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: FMICS'03
  Electronic Notes in Theoretical Computer Science, vol. 80, 2003
• The Evaluation of Full Sensitivity for Test Generation in MVL Circuits
  Elena Dubrova, Jon Muzio, and Dilian Gurov
  In Proceedings of: ISMVL'95 [941], pp. 104-109, 1995
• Full Sensitivity and Test Generation for Multiple-Valued Logic Circuits
  Elena Dubrova, Jon Muzio, and Dilian Gurov
  In Proceedings of ISMVL'94 [941], pp. 284-289, 199

Non-professional Activities

• The Origins of the Bulgars, 2007 (with slides in Bulgarian from 2014)
• Морско сърце -- a short story in Bulgarian, August 2016
• Enough!, a 6 min. improvisation, December 2003