DD's corner

Profile

I am Denisa Diaconescu, an Associate Professor at the University of Bucharest (FMI-UNIBUC), a geek enjoying a fine life, and a full-time mom.

My current research interests lie at the intersection of formal methods, consensus protocols, and decentralized systems.

I'm passionate about finding elegant solutions to hard problems, mentoring researchers, and making abstract ideas accessible through teaching and talks.

I'm currently exploring new opportunities and ideally looking for a research-focused role (protocol design, formal reasoning, system modeling) or a bridging/coordination role between technical teams and broader audiences.

I hold a BSc in Computer Science (2007) from FMI-UNIBUC, a MSc in Theoretical Computer Science (2009) from the Mathematical Institute of the Romanian Academy, and a PhD in Mathematics (2013) from FMI-UNIBUC. I was a Postdoc in George Metcalfe's group at the University of Bern (2014-2016).

Please check my Academic CV or my 1-page CV for more details, and my profiles at Google Scholar, DBLP, and LinkedIn.

Research

My research bridges formal verification, logic, and distributed systems. I’ve worked on both theoretical foundations and applied protocols. My current interests include protocol modeling, fault tolerance, and decentralized system design.

Academic Research

Formal systems in non-classical logic with applications in proof theory and knowledge representation.
Model theory and reasoning in first-order substructural logics.
Formal methods and connections between automata and logic.

Industry Research

Formalization of the Casper consensus protocol.
The theory of VLSMs, a correct-by-construction framework for describing and analyzing faulty distributed systems.
Decentralization and verification of Layer 2 protocols.

Selected List of Talks at Conferences & Workshops

ETH Bucharest 2025, Unlocking the Mystery of ZK rollups: Failures, Protections & Recoveries, Bucharest.
DeFi Security Summit 2024, Formal Verification of the INTMAX2 Protocol, Bangkok.
Encode London 2024, The Sequencer Dilemma: Balancing Decentralization and Power in Rollups, London.
10th Congress of Romanian Mathematicians 2022, VLSM: a general theory for reasoning about faulty distributed systems, Pitești (invited).
FROM 2022, An abstract framework for modelling faulty distributed systems, Jassy (invited).

Please check my Academic CV for a complete list of talks.

Selected List of Publications

ArXiv

Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems (with V. Zamfir, M. Calancea, W. Kołowski, B. Moore, K. Palmskog, T.F. Şerbănuţă, M. Stay, D. Trufaș, J. Tušil), 2022.

Journal Papers

Asynchronous Muddy Children Puzzle (work in progress) (with D. Trufaș, I. Teodorescu, T. Șerbănuță, V. Zamfir), Proceedings of the 7th Symposium on Working Formal Methods, EPTCS 389, 152-166, 2023.
Modal equivalence and bisimilarity in many-valued modal logics with many-valued accessibility relations, Fundamenta Informaticae, 173(2-3), 177-189, 2020.
Skolemization and Herbrand Theorems for Lattice-Valued Logics (with P. Cintula and G. Metcalfe), Theoretical Computer Science, 768, 54-75, 2019.
Omitting Types Theorem for Fuzzy Logics (with P. Cintula), IEEE Transactions on Fuzzy Systems, 27(2), 273-277, 2019.
A Real-Valued Modal Logic (with G. Metcalfe and L. Schnüriger), Logical Methods in Computer Science, 14(1):1-27, 2018.

Conference Papers

Intmax2: A ZK-rollup with Minimal Onchain Data and Computation Costs Featuring Decentralized Aggregators (with E. Rybakken, L. Hioki, M. Yaksetig, F. Silvasi, J. Sutherland), CoDecFin 2025.
Formalizing Correct-by-Construction Casper in Coq (with E. Li, T. Serbanuta, V. Zamfir, G. Roșu), IEEE ICBC 2020, 1-3.
Towards game semantics for nuanced logics (with Ioana Leuștean), FUZZ-IEEE 2017, 1-6.
Axiomatizing a Real-Valued Modal Logic (with G. Metcalfe and L. Schnüriger), AiML 2016, King's College Publications, 236-251, 2016.
Skolemization for Substructural Logics (with P. Cintula and G. Metcalfe), LPAR 2015, 1-15, 2015.
Exploring infinitesimal events through MV-algebras and non-Archimedean states (with A.R. Ferraioli, T. Flaminio and B. Gerla), IPMU 2014, Communications in Computer and Information Science, Vol. 443, Springer, 385-394, 2014.
A logical descriptor for regular languages via Stone duality (with S. Aguzzoli, T. Flaminio), ICTAC 2014, LNCS, Vol. 8687, Springer, 25-42, 2014.
Refinement of Structured Interactive Systems (with L. Petre, K. Sere and Gh. Ştefănescu), ICTAC 2014, LNCS, Vol. 8687, Springer, 133-150, 2014.

Please check my Academic CV for a complete list of publications, and my profiles at Google Scholar and DBLP.

Teaching

Academic Year 2024/2025

Functional Programming (Undergraduate Course, FMI-UNIBUC)
Program Verification (Master Course, FMI-UNIBUC)

Selected Past Teaching Activities

Functional Programming (Undergraduate Course, FMI-UNIBUC, 2022/2023, 2023/2024)
Program Verification (Master Course, FMI-UNIBUC, 2017/2018, 2018/2019, 2021/2022, 2022/2023, 2023/2024)
Theoretical Foundations of Programming Languages (Undergraduate Course, FMI-UNIBUC, 2021/2022, 2022/2023)
Mathematical Logic (Undergraduate Course, FMI-UNIBUC, 2018/2019)
Interactive Computation (Master Course, FMI-UNIBUC, 2016/2017 - 2018/2019)
Logic Programming (Undergraduate Course, FMI-UNIBUC, 2013/2014, 2015/2016 - 2017/2018)

Please check my Academic CV for a complete list of teaching activities.