| 2021 | FOSSACS | Leafy automata for higher-order concurrency. | Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz |
| 2021 | LICS | Verifying higher-order concurrency with data automata. | Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz |
| 2020 | CONCUR | Reachability in Fixed Dimension Vector Addition Systems with States. | Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Filip Mazowiecki |
| 2020 | TACAS | KReach: A Tool for Reachability in Petri Nets. | Alex Dixon, Ranko Lazic |
| 2019 | SODA | Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. | Wojciech Czerwinski, Laure Daviaud, Nathanal Fijalkow, Marcin Jurdzinski, Ranko Lazic, Pawel Parys |
| 2019 | STOC | The reachability problem for Petri nets is not elementary. | Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Filip Mazowiecki |
| 2018 | ICALP | When is Containment Decidable for Probabilistic Automata?. | Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Prez, James Worrell |
| 2018 | LICS | A pseudo-quasi-polynomial algorithm for mean-payoff parity games. | Laure Daviaud, Marcin Jurdzinski, Ranko Lazic |
| 2017 | ICALP | Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. | Diego Figueira, Ranko Lazic, Jrme Leroux, Filip Mazowiecki, Grgoire Sutre |
| 2017 | LICS | Timed pushdown automata and branching vector addition systems. | Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki |
| 2017 | LICS | Perfect half space games. | Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz |
| 2017 | LICS | Succinct progress measures for solving parity games. | Marcin Jurdzinski, Ranko Lazic |
| 2016 | FOSSACS | Coverability Trees for Petri Nets with Unordered Data. | Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Sylvain Schmitz, Patrick Totzke |
| 2016 | FOSSACS | Contextual Approximation and Higher-Order Procedures. | Ranko Lazic, Andrzej S. Murawski |
| 2016 | ICALP | A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. | Stefan Gller, Christoph Haase, Ranko Lazic, Patrick Totzke |
| 2016 | LICS | Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. | Matthias Englert, Ranko Lazic, Patrick Totzke |
| 2016 | LICS | The Complexity of Coverability in ν-Petri Nets. | Ranko Lazic, Sylvain Schmitz |
| 2015 | ICALP | Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. | Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz |
| 2014 | CSL | Non-elementary complexities for branching VASS, MELL, and extensions. | Ranko Lazic, Sylvain Schmitz |
| 2013 | MFCS | Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian. | Ranko Lazic, Jol Ouaknine, James Worrell |
| 2009 | VMCAI | Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. | Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski |
| 2008 | FOSSACS | Model Checking Freeze LTL over One-Counter Automata. | Stphane Demri, Ranko Lazic, Arnaud Sangnier |
| 2007 | LICS | Alternation-free modal mu-calculus for data trees. | Marcin Jurdzinski, Ranko Lazic |
| 2006 | ICFEM | Assume-Guarantee Software Verification Based on Game Semantics. | Aleksandar S. Dimovski, Ranko Lazic |
| 2006 | LICS | LTL with the Freeze Quantifier and Register Automata. | Stphane Demri, Ranko Lazic |
| 2005 | SAS | Data-Abstraction Refinement: A Game Semantic Approach. | Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic |
| 2005 | TIME | On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. | Stphane Demri, Ranko Lazic, David Nowak |
| 2004 | ICFEM | CSP Representation of Game Semantics for Second-Order Idealized Algol. | Aleksandar S. Dimovski, Ranko Lazic |
| 2004 | IFM | Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. | Xu Wang, A. W. Roscoe, Ranko Lazic |
| 2000 | CONCUR | A Unifying Approach to Data-Independence. | Ranko Lazic, David Nowak |
| 1999 | PDPTA | Data Independence with Generalised Predicate Symbols. | Ranko Lazic, Bill Roscoe |