Prof. Dr. Ciprian Teodorov

Ciprian Teodorov is a Full Professor at ENSTA | Institut Polytechnique de Paris and a senior researcher in the P4S team of the Lab-STICC Laboratory. His research spans executable models, formal verification, model-driven engineering (MDE), and model-based systems engineering (MBSE), focusing on system-level behavioral analysis and toolchain integration.

Prof. Teodorov leads the OBP2 Semantic Diagnosis & Formal Verification team, developing unified execution and verification frameworks that bridge domain-specific modeling with formal analysis. He introduced the G∀min∃ methodology advocating for semantic-level verification over traditional model transformation approaches, which often lead to semantic divergence and costly equivalence proofs. The *G∀min∃ Semantic Language Interface (SLI)* provides a modular architecture to formalize and connect the dynamic semantics of modeling languages with verification tools.

Prof. Teodorov is the author of over 60 publications and has been an active member of INCOSE since 2016. Before entering academia, he worked at Dolphin Integration as an EDA/CAD Software Engineer, contributing to the design of the SMASH mixed-signal simulator.

He earned his Ph.D. in Computer Science from the University of Western Brittany, where he proposed novel physical-design frameworks targeting agile, model-driven co-exploration of architecture and CAD toolchains at the nanoscale.

Multiverse Debugging: Toward Behavioral Transparency Across Industrial Design Languages

Abstract

Modern system design relies heavily on modeling languages, like UML, which are widely adopted in industry but often disconnected from the formal tools used to analyze and verify behavior. This gap between intuitive design and rigorous analysis limits the practical application of formal methods in everyday engineering workflows.

Multiverse debugging addresses this challenge by treating system behavior as a structured space of possible executions, a “multiverse” that designers can explore interactively. Instead of relying on brittle syntactic transformations, this approach uses a language-independent semantic interface to connect domain-specific models directly to behavioral analysis tools. The result is a scalable, intuitive debugging experience that extends traditional breakpoints with temporal and multiverse-aware breakpoints, enabling fine-grained analysis of concurrency and non-determinism. Applied to UML, and similar languages, this method preserves design intent while providing deep behavioral insights.

This keynote introduces multiverse debugging as a practical bridge between high-level modeling and formal analysis, grounded in a broader vision focused on semantic fidelity and software maintainability across heterogeneous specifications. The approach empowers engineers to better understand, validate, and communicate system behavior, bringing formal reasoning closer to the design desk.