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.

Research Interest

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

Education

• 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

Publications

1. Balasubramanian A.R., J. Esparza, M. Lazić: Complexity of Verification and Synthesis of Threshold Automata, accepted to ATVA 2020
2. 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.
3. É. 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.
4. É. 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.
5. 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.
6. 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.
7. C. Drăgoi, M. Lazić, J. Widder: Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto [pdf], in: Sinteza, pages 131-138, 2018.
8. 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.
9. 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.
10. 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.
11. 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.