Research

In general, my research focuses on the formal specification and verification of distributed, component-based systems. Specifically, I am working on the integration of automatic (Model Checking, Runtime Verification) and semi-automatic (Interactive Theorem Proving) techniques for the verification of such systems.
Recently, I am applying these techniques for the formalization and verification of Blockchain-related protocols.

Selected Publications

D. Marmsoler and A. Brucker (2021)
A Denotational Semantics of Solidity in Isabelle/HOL (Link)
19th International Conference on Software Engineering and Formal Methods.

D. Marmsoler and A. Petrovska (2020)
Runtime Verification for Dynamic Architectures (Link)
Journal of Logical and Algebraic Methods in Programming.

D. Marmsoler and Genc Blakqori (2019)
APML: An Architecture Proof Modeling Language (Link)
Third World Congress on Formal Methods.

D. Marmsoler (2019)
A calculus for dynamic architectures (Link)
Science of Computer Programming.

D. Marmsoler and Habtom K. Gidey (2019)
Interactive Verification of Architectural Design Patterns in FACTum (Link)
Formal Aspects of Computing.

D. Marmsoler (2019)
Towards Verified Blockchain Architectures:
A Case Study on Interactive Architecture Verification (Link)
39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems.

D. Marmsoler (2018)
Hierarchical Specification and Verification of Architectural Design Patterns (Link)
21st International Conference on Fundamental Approaches to Software Engineering.