| LTL with the freeze quantifier and register automata S Demri, R Lazić ACM Transactions on Computational Logic (TOCL) 10 (3), 1-30, 2009 | 395 | 2009 |
| The reachability problem for Petri nets is not elementary W Czerwiński, S Lasota, R Lazić, J Leroux, F Mazowiecki Journal of the ACM (JACM) 68 (1), 1-28, 2020 | 214 | 2020 |
| A semantic study of data independence with applications to model checking. RS Lazic University of Oxford, 1999 | 192* | 1999 |
| Nets with tokens which carry data R Lazić, T Newcomb, J Ouaknine, AW Roscoe, J Worrell Fundamenta Informaticae 88 (3), 251-274, 2008 | 159 | 2008 |
| Succinct progress measures for solving parity games M Jurdziński, R Lazić 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-9, 2017 | 128 | 2017 |
| Alternating automata on data trees and XPath satisfiability M Jurdziński, R Lazić ACM Transactions on Computational Logic (TOCL) 12 (3), 19, 2011 | 124* | 2011 |
| On the freeze quantifier in constraint LTL: decidability and complexity S Demri, R Lazić, D Nowak Information and Computation 205 (1), 2-24, 2007 | 109 | 2007 |
| The covering and boundedness problems for branching vector addition systems S Demri, M Jurdziński, O Lachish, R Lazić Journal of Computer and System Sciences 79 (1), 23-38, 2013 | 77* | 2013 |
| Model checking freeze LTL over one-counter automata S Demri, R Lazić, A Sangnier International Conference on Foundations of Software Science and …, 2008 | 71* | 2008 |
| A unifying approach to data-independence R Lazić, D Nowak International Conference on Concurrency Theory, 581-596, 2000 | 69 | 2000 |
| The reachability problem for two-dimensional vector addition systems with states M Blondin, M Englert, A Finkel, S Göller, C Haase, R Lazić, P McKenzie, ... Journal of the ACM (JACM) 68 (5), 1-43, 2021 | 68* | 2021 |
| Fixed-dimensional energy games are in pseudo-polynomial time M Jurdziński, R Lazić, S Schmitz International Colloquium on Automata, Languages, and Programming, 260-272, 2015 | 64 | 2015 |
| Nonelementary complexities for branching VASS, MELL, and extensions R Lazić, S Schmitz ACM Transactions on Computational Logic (TOCL) 16 (3), 1-30, 2015 | 63 | 2015 |
| Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games W Czerwiński, L Daviaud, N Fijalkow, M Jurdziński, R Lazić, P Parys Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete …, 2019 | 58 | 2019 |
| Data-abstraction refinement: A game semantic approach A Dimovski, DR Ghica, R Lazić International Static Analysis Symposium, 102-117, 2005 | 50* | 2005 |
| Safety alternating automata on data words R Lazić ACM Transactions on Computational Logic (TOCL) 12 (2), 10, 2011 | 48* | 2011 |
| The ideal view on Rackoff’s coverability technique R Lazić, S Schmitz International Workshop on Reachability Problems, 76-88, 2015 | 47* | 2015 |
| What makes Petri nets harder to verify: stack or data? R Lazić, P Totzke Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William …, 2016 | 39* | 2016 |
| Compositional software verification based on game semantics and process algebra A Dimovski, R Lazić International Journal on Software Tools for Technology Transfer 9 (1), 37-51, 2007 | 35* | 2007 |
| A pseudo-quasi-polynomial algorithm for mean-payoff parity games L Daviaud, M Jurdziński, R Lazić Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 32 | 2018 |
Bill Roscoe (A.W. Roscoe)Emeritus Professor of Computer Science, Oxford UniversityVerified email at cs.ox.ac.uk
