Marijana Lazić

About Me

I am 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, since June 2019.

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.

You can download my CV here (updated in September 2021).

I am on maternity leave until the end of June 2022.

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, 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)
  2. 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
  3. 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.
  4. 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
  5. 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.
  6. É. 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.
  7. É. 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.
  8. 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.
  9. 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.
  10. C. Drăgoi, M. Lazić, J. Widder: Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto [pdf], in: Sinteza, pages 131-138, 2018.
  11. 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.
  12. 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.
  13. 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.
  14. 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