Marijana Lazić

About Me

I was a postdoc at the Chair for Foundations of Software Reliability and Theoretical Computer Science at TU Munich, working in the group of Javier Esparza, within the ERC-supported project PaVeS, from June 2019 until September 2023.

Previously, I was a PhD student in the Doctoral College LogiCS, and a project assistant in the FORSYTE group at TU Wien, supervised by Josef Widder and Igor Konnov.

Currently, I am working at TWT GmbH Science & Innovation in the team for Model Based Systems Engineering and Autonomous Driving.

You can download my CV here (updated in August 2023).

Research Interest

Formal methods, Parameterized Model Checking, Verification and Synthesis of Fault Tolerant Distributed Algorithms, Knowledge and Topology in Distributed Computing


  • PhD in Computer Science, TU Wien, June 2019
    Supervisors: Josef Widder and Igor Konnov
    Topic: Reduction Techniques for Parameterized Model Checking and Synthesis of Fault-Tolerant Distributed Algorithms [pdf]

  • MSc in Mathematics, University of Novi Sad, September 2012
    Supervisor: Rozalija Madaras
    Topic: Power Structures and Multialgebras [pdf] (in Serbian)

  • Bachelor in Mathematics, University of Novi Sad, September 2011


  1. N. Bertrand, V. Gramoli, I. Konnov, M. Lazić, P. Tholoniat, J. Widder: Brief Announcement: Holistic Verification of Blockchain Consensus [doi], in: ACM Symposium on Principles of Distributed Computing (PODC 2022): 424-426, 2022
  2. N. Bertrand, V. Gramoli, I. Konnov, M. Lazić, P. Tholoniat, J. Widder: Holistic Verification of Blockchain Consensus [doi], in: 36th International Symposium on Distributed Computing (DISC 2022): 10:1-10:24, 2022
  3. N. Bertrand, I. Konnov, M. Lazić, J. Widder: Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries [doi], in: International Journal on Software Tools for Technology Transfer. (2021)
  4. N. Bertrand, M. Lazić, J. Widder: A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries [pdf] [hal], in: 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021), 219-239, 2021
  5. H. van Ditmarsch, É. Goubault, M. Lazić, J. Ledent, S. Rajsbaum: A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks [doi], in: Journal of Logical and Algebraic Methods in Programming., vol. 121, 26 p., 100662, 2021
  6. Balasubramanian A.R., J. Esparza, M. Lazić: Complexity of Verification and Synthesis of Threshold Automata [pdf] [arxiv], in: 18ᵗʰ International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), Lecture Notes in Computer Science, vol. 12302, pages 144-160, 2020
  7. I. Konnov, M. Lazić, I. Stoilkovska, J. Widder: Tutorial: Parameterized Verification with Byzantine Model Checker [pdf], in: Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020), pages 189-207, 2020.
  8. É. Goubault, M. Lazić, J. Ledent, S. Rajsbaum: A dynamic epistemic logic analysis of the equality negation task [pdf], in: Dynamic Logic. New Trends and Applications - Second International Workshop, DaLí, pages 53-70, 2019.
  9. É. Goubault, M. Lazić, J. Ledent, S. Rajsbaum: Wait-free Solvability of Equality Negation Tasks [pdf], in: 33rd International Symposium on Distributed Computing (DISC 2019), vol. 146 of LIPIcs, pages 21:1-21:16, 2019.
  10. N. Bertrand, I. Konnov, M. Lazić, J. Widder: Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries  [pdf] [preprint+proofs], in: 30th International Conference on Concurrency Theory (CONCUR 2019), volume 140 of LIPIcs, pages 33:1-33:15, 2019.
  11. I. Berkovits, M. Lazić, G. Losa, O. Padon, S. Shoham: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics [pdf+proofs] [doi], in: Computer Aided Verification (CAV) 2019. Lecture Notes in Computer Science, vol. 11562, pages 245-266, 2019.
  12. C. Drăgoi, M. Lazić, J. Widder: Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto [pdf], in: Sinteza, pages 131-138, 2018.
  13. M. Lazić, I. Konnov, J. Widder, R. Bloem: Synthesis of Distributed Algorithms with Parameterized Threshold Guards [pdf], OPODIS, vol. 95 of LIPIcs, pages 32:1-32:20, 2017.
  14. I. Konnov, M. Lazić, H. Veith, J. Widder: Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms [pdf], in: Formal Methods in System Design, Springer, 2017.
  15. I. Konnov, M. Lazić, H. Veith, J. Widder: A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms [pdf] [preprint+proofs] in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
  16. E. Aichinger, M. Lazić, N. Mudrinski, Finite generation of congruence preserving functions [pdf] [doi], in: Monatshefte für Mathematik, volume 181, pages 35–62, 2016.



  • Email: lazic [at]

  • Phone: +49-89-289-17230

  • Office: 3.11.057 (3rd floor, 11th hallway, one of the last offices on the left)

  • Mailing Address:

Institut für Informatik (I7)

Technische Universität München

Boltzmannstr. 3

85748 Garching b. München, Germany