Marijana Lazić

I graduated in June 2019, and since then I work as a postdoc at TU Munich with Javier Esparza. Check out my new web page here.


Marijana Lazić
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien

Room: HA 03 05 (how to get there)
Phone: +43 (1) 58801 – 740 077
Email: ta.etysrofnull@cizal

© Sara Meister

Research Interests

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


Current Position


Research Visits

  • Oct. 2016—Dec. 2016: Prakash Panangaden and Vijay D’Silva, Simons Institute for the Theory of Computing, University of California, Berkeley
  • Jun. 2017—Jul. 2017 and Nov. 2017—Dec. 2017: Yoram Moses, Technion, Israel Institute of Technology, Haifa, Israel



[6] Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
Nathalie Bertrand, Igor Konnov, Marijana Lazic, Josef Widder
HAL, volume hal-01925533, Nov 2018.
[bibtex] [pdf]
[5] Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto
Cezara Dragoi, Marijana Lazic, Josef Widder
Sinteza, pages 131-138, 2018.
[bibtex] [pdf]
[4] Synthesis of Distributed Algorithms with Parameterized Threshold Guards
Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem
OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017.
[bibtex] [pdf]
[3] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
Note: A pre-print including the proofs is available at
[bibtex] [pdf]
[2] Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, volume 51, number 2, pages 270-307, 2017, Springer.
[bibtex] [pdf]
[1] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]


Master thesis & Previous publications

Latest News

LogicLounge in memoriam Helmut Veith

Will robots take away your job? In memory of Helmut Veith, this year’s Conference on Computer Aided Verification (CAV), which takes place in Toronto, will feature a LogicLounge on the effect of automation and artificial intelligence on our jobs.

Continue reading

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

Full news archive