Fakultät für Informatik TU München - Fakultät für Informatik
Lehrstuhl IV: Software & Systems Engineering
Technische Universität München

Diego Marmsoler
M.Sc. with honours

Diego Marmsoler

Technische Universität München
Institut für Informatik – Lehrstuhl IV (I4)
Boltzmannstr. 3
85748 Garching bei München

Room 00.11.058

Phone +49 89 289-17882
Fax +49 89 289-17307

Office Hours
please call/mail ahead for an appointment

I'm always looking for students interested in Modeling of Software Architectures, Formal Methods, and related topics. Currently, I have open topics (for thesis or guided research) in the following areas:
  • Modeling Architecture Design Patterns in Eclipse/EMF
  • Analysis of Blockchain Architectures
If this sounds interesting for you then just write me an and I would be glad to present the topics in more detail!

About Me

    After finishing my bachelor in Applied Computer Science at the Free University of Bozen-Bolzano, I studied in the Software Engineering Elite Graduate Program at the TU München, LMU, and Augsburg University. For my masters thesis, I had the opportunity to work together with C.A.R. Hoare at Microsoft Research in Cambridge. Since March 2013 I'm employed as a research assistant and PhD candidate at the chair for Software & Systems Engineering at Technische Universität München. I do have more than 4 years of professional experience as a Software Engineer and Technical Consultant. I was awarded the IEEE Computer Society Best Undergraduate Paper Award, the 3th place in the IEEE Region 8 Student Paper Contest, and finalist in the ACM Student Research Competition. In my doctoral thesis I'm concerned with formalizing and analyzing software architecture styles.

Fields of interest

  • Software Architectures
  • Formal System Models
  • Foundations of Software Engineering


  • SiBaSe (Sicherheitsbaukasten für sichere Eingebettete Systeme)
    In this project we are concerned with availability issues in the context of software security. We are working on a formal language to express availability requirements for single components.
  • Firmament
    In this project we investigate implications of architecture decisions to software quality. To this end we also explore the possibilities of design-by-contract approaches.
  • Future-Proof Architectures
    In this project we investigate requirements for future architectures and how to address them.


Selected Publications


  • D. Marmsoler and Leo Eichhorn (2018)
    Simulation-Based Analysis of Blockchain Architectures (Link)
    The 3rd Symposium on Distributed Ledger Technology.

  • D. Marmsoler (2018)
    A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL (Link)
    The 20th International Conference on Formal Engineering Methods.

  • D. Marmsoler and H. K. Gidey (2018)
    FACTUM Studio: A Tool for the Axiomatic Specification and Verification of Architectural Design Patterns (Link)
    15th International Conference on Formal Aspects of Component Software.

  • D. Marmsoler (2018)
    On Syntactic and Semantic Dependencies in Service-Oriented Architectures (Link)
    12th International Symposium on Theoretical Aspects of Software Engineering.

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

  • D. Marmsoler (2018)
    A Theory of Architectural Design Patterns (Link)
    Archive of Formal Proofs.

  • D. Marmsoler (2017)
    Towards a Calculus for Dynamic Architectures (Link)
    14th International Colloquium on Theoretical Aspects of Computing.

  • D. Marmsoler (2017)
    Dynamic Architectures (Link)
    Archive of Formal Proofs.

  • D. Marmsoler, M. Gleirscher (2017)
    On Activation, Connection, and Behavior in Dynamic Architectures (Link)
    Scientific Annals of Computer Science. Volume XXVI, Issue 2, 2016.

  • D. Marmsoler (2017)
    On the Semantics of Temporal Specifications of Component-Behavior for Dynamic Architectures (Link)
    11th International Symposium on Theoretical Aspects of Software Engineering.

  • H. K. Gidey, D. Marmsoler, J. Eckhardt (2017)
    Grounded Architectures: Using Grounded Theory for the Design of Software Architectures (Link)
    International Workshop on decision Making in Software ARCHitecture.

  • D. Marmsoler, S. Degenhardt (2017)
    Verifying Patterns of Dynamic Architectures Using Model Checking (Link)
    14th International Workshop on Formal Engineering approaches to Software Components and Architectures.

  • S. Kugele, D. Marmsoler, N. Mata, K. Werner (2016)
    Verification of Component Architectures using Mode-Based Contracts (Link)
    14th International Conference on Formal Methods and Models for System Design.

  • D. Marmsoler, M. Gleirscher (2016)
    Specifying Properties of Dynamic Architectures using Configuration Traces (Link)
    13th International Colloquium on Theoretical Aspects of Computing.

  • A. Malkis, D. Marmsoler (2015)
    A Model of Service-Oriented Architectures (Link)
    9th Brazilian Symposium on Software Components, Architectures, and Reuse.

  • D. Marmsoler, A Malkis, J Eckhardt (2015)
    A Model of Layered Architectures (Link)
    12th International Workshop on Formal Engineering approaches to Software Components and Architectures.

  • D. Marmsoler (2014)
    Towards a Theory of Architectural Styles (Link)
    22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering.

  • D. Marmsoler (2013)
    On the Laws of Failure: A Theory of Compensable Programs (Link)
    15th International Conference on Computer as a Tool.


  • D. Marmsoler (2013)
    On the Laws of Failure: A Theory of Compensable Programs (Link)
    This work identifies three basic programming concepts used for error handling and investigates the laws governing these concepts. A trace semantics for exception handling, longrunning transactions and recovery blocks is given and 11 basic laws are derived. Algebraic reasoning is used to derive three more properties on top of these basic laws. An assumption about the existence of an inverse program is investigated and two direct consequences are provided. The assumption is weakened to address practical issues and a proof obligation is provided to obtain the properties anyway. The work is based on the algebraic method and provides a novel approach to completely specify a program in terms of commonalities and differences w.r.t. another program. Furthermore, all proofs are stated exclusively in Isabelle/Isar, thus they are mechanically checked, though human readable.

  • D. Marmsoler (2010)
    Applying the Scientific Method in the Definition and Analysis of a new Architectural Style (Link)
    Refined experience in form of architectural styles is considered as one of the "Grand Tools" in the design of new software systems. However, current approaches to define and investigate such architectural styles lack rigor and reliability. Hence this text presents the Architectural Style Analysis Method derived from application of the scientific method to the definition and analysis of software architectural styles. Furthermore the text identifies the Partial Refinement architectural style observed in Microsoft’s Dynamics AX product line. ASAM is further applied to define and investigate this new architectural style. Thus, the style is first defined formally, depicting its elements and decomposing them into "architectural primitives"; thereby a new kind of connector is identified and analyzed in detail. Then a set of software metrics is derived to guide the empirical observation of the style in action and two tools are presented to collect measures for the specified metrics. The results of the empirical observation are presented and a statistical analysis of the obtained data follows. Finally a set of related hypotheses is derived on top of this analysis to state formally some of the properties elicited by the style.