Denna tjänst avvecklas 2026-01-19. Läs mer här ( länk ) Dilian Gurov's Publications
Denna tjänst avvecklas 2026-01-19. Läs mer här ( länk ) Dilian Gurov's Publications
Latest update: 1 October 2025
Multi-agent strategic planning
Contracts for software development
An Expressive Trace Logic for Recursive Programs FSCD'25 LIPIcs, vol. 337, pp. 21:1–21:22, 2025 Machine-Checked
Compositional Specification and Proofs for Embedded Systems TASE'25 Lecture Notes in Computer Science , vol. 15841, pp. 67-82, 2025Post-Hoc
Formal Verification of Automotive Software with Informal
Requirements: An Experience Report RE'24 Deductively Verified Program Models
for Software Model Checking An Exercise in Mind Reading: Automatic Contract Inference for
Frama-C Guide to Software Verification with Frama-C , 2024Trace-based
Deductive Verification '23 EPiC Series in Computing , vol. 94, pp. 73-95, 2023Contract
Based Embedded Software Design TASE'23 Lecture Notes in Computer Science , vol. 13931, pp. 77-94, 2023Principles
of Contract Languages - Report from Dagstuhl Seminar 22451 Deductive
Verification Based Abstraction for Software Model Checking ISoLA'22 Lecture Notes in Computer Science , vol. 13701, pp. 7-28, 2022Alice
in Wineland: A Fairy Tale with Contracts The Logic of Software. A Tasting Menu
of Formal Methods Lecture Notes in Computer Science , vol. 13360, pp. 229-242,
2022An
Abstract Contract Theory for Programs with Procedures FASE'21 Lecture Notes in Computer Science , vol. 12649, pp. 152-171,
2021 (full
version )Formally
Proving Compositionality in Industrial Systems with Informal
Specifications ISoLA'20 Lecture Notes in Computer Science , vol. 12478, pp. 348-365,
2020Constraint-Based
Contract Inference for Deductive Verification Deductive Software Verification Lecture Notes in Computer Science , vol. 12345, pp. 149-176,
2020A
Hoare Logic Contract Theory: An Exercise in Denotational Semantics Principled Software Development
Software verification
Automatic
Program Instrumentation for Automatic Verification CAV'23 Lecture Notes in Computer Science , vol. 13966, pp. 281-304,
2023CAV Distinguished Paper Award 2023 Bounded
Invariant Checking for Stateflow Programs full version )Dynamic
Vulnarability Detection on Smart Contracts Using Machine Learning
EASE'21 ACM , pp. 305-312, 2021An
Abstraction Technique for Verifying Shared-Memory Concurrency Applied Sciences , vol. 10, no. 11,
pp. 1-48, 2020Practical
Abstractions for Automated Verification of Shared-Memory
Concurrency VMCAI'20 Lecture Notes in Computer Science , vol. 11990, pp. 401-425,
2020
Formal
Verification in Automotive Industry: Enablers and Obstacles ISoLA'18 Lecture Notes in Computer Science , vol. 11247, pp. 139-158,
2018Specification
and Verification of Synchronization with Condition Variables Science of Computer Programming ,
vol. 163, pp. 174-189, 2018Deductive
Functional Verification of Safety-Critical Embedded C-Code: An
Experience Report FMICS-AVOCS'17 Lecture Notes in Computer Science , vol. 10471, pp. 3-18, 2017An
Abstraction Technique for Describing Concurrent Program Behaviour VSTTE'17 Lecture Notes in Computer Science , vol. 10712, pp. 191-209,
2017Formal Architecture Modeling of Sequential
Non-recursive C Programs Science of Computer Programming , vol.
146, pp. 2-27, 2017Specification
and Verification of Synchronization with Condition Variables FTSCS'16 Communications in Computer and Information Science , vol. 694,
pp. 3-19, 2017Provably
Correct Control Flow Graphs from Java Bytecode Programs with
Exceptions Software Tools for Technology Transfer ,
vol. 18, no. 6, pp. 653-684, 2016Short
version appeared in Proceedings of: SEFM'12 Lecture Notes in Computer Science , vol. 7504, pp. 33-47, 2012Sound
Control Flow Graph Extraction from Incomplete Java Bytecode
Programs FASE '14 Lecture Notes in Computer Science , vol. 8411, pp. 215-229, 2014Program
Models for Compositional Verification ICFEM'0 8Lecture Notes in Computer Science , vol. 5256, pp. 147-166, 2008
Logics of programs
Soundness
and Completeness of a Model-Checking Proof System for CTL mu-Calculus
with Explicit Points and Approximations 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 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 '22 , Volume BACM , pp. 132-139, 2022Category
Theory Framework for Variability Models with Non-Functional
Requirements CAiSE'21 Lecture Notes in Computer Science , vol. 12751, pp. 397-413,
2021Self-Correlation
and Maximum Independence in Finite Relations FICS'15 Electronic Proceedings in Theoretical Computer Science , vol.
191, pp. 60-74, 2015Model
Mining and Efficient Verification of Software Product Lines Serdica Journal of Computing , vol. 9,
no. 1, pp. 35-82, 2015A
Hierarchical Variability Model for Software Product Lines ISoLa'11 Communications in Computer and Information Science , vol. 336,
pp. 181-199, 2012 Compositional
Algorithmic Verification of Software Product Lines 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 Science of Computer Programming , vol.
127, pp. 76-102, 2016Short
version appeared in Proceedings of: FACS'14 Lecture Notes in Computer Science , vol. 8997, pp. 327-345, 2015Procedure-Modular
Specification and Verification of Temporal Safety Properties Software and Systems Modeling , vol.
14, no. 1, pp. 83-100, February 2015Short
version appeared in Proceedings of: SEFM'11 Lecture Notes in Computer Science , vol. 7041, pp. 366-381, 2011Reducing
Behavioural to Structural Properties of Programs with Procedures Theoretical Computer Science , vol.
480, pp. 69-103, 2013Short
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 FoVeOOS'10 Lecture Notes in Computer Science , vol. 6528, pp. 107-121, 2010Procedure-Modular
Verification of Control Flow Safety Properties FTfJP'10 , ACM Digital Library, 2010Compositional
Verification of Sequential Programs with Procedures Journal of Information and Computation ,
vol. 206, no. 7, pp. 840-868, 2008Composing
Modal Properties of Programs with Procedures FESCA'07 Electronic Notes in Theoretical Computer Science , vol. 203,
issue 7, pp. 87-101, 2009 (slides )Interface
Abstraction for Compositional Verification SEFM'05 IEEE Computer Society , pp. 414-423, 2005 (slides )Compositional Verification for Secure Loading of
Smart Card Applets Memocode'04 IEEE Formal Methods and Models for Co-Design , pp. 211-222, 2004Checking
Absence of Illicit Applet Interactions: A Case Study FASE'04 Lecture Notes in Computer Science , vol. 2984, pp. 84-98 EASST
award for Best Software Science Paper slides ) Simulation Logic, Applets and Compositional
Verification Temporal
Logic and Toolset for Applet Verification: Compositional
Reasoning, Model Checking, Abstract Interpretation Model
Checking of Multi-Applet JavaCard Applications CARDIS'02 slides )Compositional
Verification of Secure Applet Interactions 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 FTfJP'01 , 2001
Security and privacy
Privacy Preserving Business Process Matching PST'15 , IEEE, pp. 36-43, 2015 Business
Process Engineering and Secure Multiparty Computation Applications of Secure Multiparty Computation Privacy Preserving Business Process Fusion BPM-WS'14 Lecture Notes in Business Information Processing , vol. 202, pp.
96-101, 2015Private Intersection of Regular Languages PST'14 , IEEE, pp. 112-120, 2014Provably
Correct Runtime Monitoring Journal of Logic and Algebraic
Programming , vol. 78, pp. 304-339, 2009Short version appeared in Proceedings of: FM'0 8Lecture Notes in Computer Science , vol. 5014, pp. 262-277, 2008
(slides )
State space representations for verification of open systems
Verification of peer-to-peer algorithms
Verification
of Peer-to-peer Algorithms: A Case Study MTCoord'06 Electronic Notes in Theoretical Computer Science , vol. 181, pp.
35-47, 2007Verifying
a Structured Peer-to-peer Overlay Network: The Static Case 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 Software Tools for Technology Transfer ,
vol. 4, pp. 405-420, 2003 Semi-Automated
Verification of Erlang Code ASE'01 long version )The
Erlang Verification Tool 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 FMICS 2000 GMD Report, no. 91, pp. 109-122, 2000 A
Framework for Formal Reasoning about Open Distributed Systems ASIAN'99 Lecture Notes in Computer Science, vol. 1742, pp. 87-100, 1999
Compositional
Verification of CCS Processes PSI'99 Lecture Notes in Computer Science, vol. 1755, pp. 247-256,
2000 System
Description: Verification of Distributed Erlang Programs CADE'98 Lecture Notes in Artificial Intelligence, vol. 1421, pp.
38-41, 1998Toward
Parametric Verification of Open Distributed Systems Compositionality: The Significant Difference Lecture Notes in Computer Science, vol. 1536, pp. 150-185,
1998 Specification
and Verification of Communicating Systems with Value Passing A
Compositional Proof System for the Modal mu-calculus and CCS CMU Techreport CMU-CS-97-105 , 1997 A Modal mu-Calculus and a Proof System for Value
Passing Processes INFINITY'96 Electronic Notes in Theoretical Computer Science, Vol.5, 1996
Other
Formal
Methods Research at SICS and KTH: An Overview FMICS'03 Electronic Notes in Theoretical Computer Science, vol. 80, 2003
The
Evaluation
of Full Sensitivity for Test Generation in MVL Circuits ISMVL'95 [941], pp. 104-109, 1995Full
Sensitivity
and Test Generation for Multiple-Valued Logic Circuits ISMVL'94 [941], pp. 284-289, 199
Non-professional Activities
Inner:
1280 x 559