Data Independence with Generalised Predicate Symbols. - Ranko Lazic 001; Bill Roscoe (PDPTA, 1999)

A semantic study of data independence with applications to model checking. - Ranko S. Lazic (1999)

A Unifying Approach to Data-Independence. - Ranko Lazic 001; David Nowak (CONCUR, 2000)

On a Semantic Definition of Data Independence . - Ranko Lazic 001; David Nowak (TLCA, 2003)

On Model Checking Data-Independent Systems with Arrays with Whole-Array Operations. - Ranko Lazic 001; Thomas Christopher Newcomb; A. W. Roscoe 001 (25 Years Communicating Sequential Processes, 2004)

CSP Representation of Game Semantics for Second-Order Idealized Algol. - Aleksandar S. Dimovski; Ranko Lazic 001 (ICFEM, 2004)

Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. - Xu Wang 001; A. W. Roscoe 001; Ranko Lazic 001 (IFM, 2004)

Software Model Checking Based on Game Semantics and CSP. - Aleksandar S. Dimovski; Ranko Lazic 001 (AVoCS, 2004)

Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification. - Ranko Lazic 001 (INFINITY, 2004)

Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting. - Ranko Lazic 001; Thomas Christopher Newcomb; Bill Roscoe (INFINITY, 2004)

On model checking data-independent systems with arrays without reset. - Ranko Lazic 001; Thomas Christopher Newcomb; A. W. Roscoe 001 (Theory Pract. Log. Program., 2004)

Abstraction-refinement for game-based model checking. - Aleksandar S. Dimovski; Dan R. Ghica; Ranko Lazic 001 (GALOP@ETAPS, 2005)

Data-Abstraction Refinement: A Game Semantic Approach. - Aleksandar S. Dimovski; Dan R. Ghica; Ranko Lazic 001 (SAS, 2005)

On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. - Stéphane Demri; Ranko Lazic 001; David Nowak (TIME, 2005)

Preface. - Ranko Lazic 001; Rajagopal Nagarajan (AVoCS, 2005)

Safely Freezing LTL. - Ranko Lazic 001 (FSTTCS, 2006)

Assume-Guarantee Software Verification Based on Game Semantics. - Aleksandar S. Dimovski; Ranko Lazic 001 (ICFEM, 2006)

LTL with the Freeze Quantifier and Register Automata. - Stéphane Demri; Ranko Lazic 001 (LICS, 2006)

A Counterexample-Guided Refinement Tool for Open Procedural Programs. - Aleksandar S. Dimovski; Dan R. Ghica; Ranko Lazic 001 (SPIN, 2006)

Nets with Tokens Which Carry Data. - Ranko Lazic 001; Thomas Christopher Newcomb; Joël Ouaknine; A. W. Roscoe 001; James Worrell 001 (ICATPN, 2007)

Alternation-free modal mu-calculus for data trees. - Marcin Jurdzinski; Ranko Lazic 001 (LICS, 2007)

Guest Editorial. - Ranko Lazic 001; Rajagopal Nagarajan (Formal Aspects Comput., 2007)

Compositional software verification based on game semantics and process algebra. - Aleksandar S. Dimovski; Ranko Lazic 001 (Int. J. Softw. Tools Technol. Transf., 2007)

Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. - Patricia Bouyer; Thomas Brihaye; Marcin Jurdzinski; Ranko Lazic 001; Michal Rutkowski (FORMATS, 2008)

Model Checking Freeze LTL over One-Counter Automata. - Stéphane Demri; Ranko Lazic 001; Arnaud Sangnier (FoSSaCS, 2008)

The Covering and Boundedness Problems for Branching Vector Addition Systems. - Stéphane Demri; Marcin Jurdzinski; Oded Lachish; Ranko Lazic 001 (FSTTCS, 2009)

Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. - Marcin Jurdzinski; Ranko Lazic 001; Michal Rutkowski (VMCAI, 2009)

The reachability problem for branching vector addition systems requires doubly-exponential space. - Ranko Lazic 001 (Inf. Process. Lett., 2010)

Data-abstraction refinement: a game semantic approach. - Adam Bakewell; Aleksandar S. Dimovski; Dan R. Ghica; Ranko Lazic 001 (Int. J. Softw. Tools Technol. Transf., 2010)

Model checking memoryful linear-time logics over one-counter automata. - Stéphane Demri; Ranko Lazic 001; Arnaud Sangnier (Theor. Comput. Sci., 2010)

Alternating automata on data trees and XPath satisfiability. - Marcin Jurdzinski; Ranko Lazic 001 (ACM Trans. Comput. Log., 2011)

Safety alternating automata on data words. - Ranko Lazic 001 (ACM Trans. Comput. Log., 2011)

Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian. - Ranko Lazic 001; Joël Ouaknine; James Worrell 001 (MFCS, 2013)

The reachability problem for vector addition systems with a stack is not elementary. - Ranko Lazic 001 (CoRR, 2013)

Non-elementary complexities for branching VASS, MELL, and extensions. - Ranko Lazic 001; Sylvain Schmitz (CSL-LICS, 2014)

Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. - Marcin Jurdzinski; Ranko Lazic 001; Sylvain Schmitz (ICALP (2), 2015)

The Ideal View on Rackoff's Coverability Technique. - Ranko Lazic 001; Sylvain Schmitz (RP, 2015)

Nonelementary Complexities for Branching VASS, MELL, and Extensions. - Ranko Lazic 001; Sylvain Schmitz (ACM Trans. Comput. Log., 2015)

Coverability Trees for Petri Nets with Unordered Data. - Piotr Hofman; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Sylvain Schmitz; Patrick Totzke (FoSSaCS, 2016)

Contextual Approximation and Higher-Order Procedures. - Ranko Lazic 001; Andrzej S. Murawski (FoSSaCS, 2016)

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. - Stefan Göller; Christoph Haase; Ranko Lazic 001; Patrick Totzke (ICALP, 2016)

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. - Matthias Englert; Ranko Lazic 001; Patrick Totzke (LICS, 2016)

The Complexity of Coverability in ν-Petri Nets. - Ranko Lazic 001; Sylvain Schmitz (LICS, 2016)

Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete. - Ranko Lazic 001; Joël Ouaknine; James Worrell 001 (ACM Trans. Comput. Log., 2016)

What Makes Petri Nets Harder to Verify: Stack or Data? - Ranko Lazic 001; Patrick Totzke (Concurrency, Security, and Puzzles, 2017)

Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. - Diego Figueira; Ranko Lazic 001; Jérôme Leroux; Filip Mazowiecki; Grégoire Sutre (ICALP, 2017)

Timed pushdown automata and branching vector addition systems. - Lorenzo Clemente; Slawomir Lasota 001; Ranko Lazic 001; Filip Mazowiecki (LICS, 2017)

Perfect half space games. - Thomas Colcombet; Marcin Jurdzinski; Ranko Lazic 001; Sylvain Schmitz (LICS, 2017)

Succinct progress measures for solving parity games. - Marcin Jurdzinski; Ranko Lazic 001 (LICS, 2017)

When is Containment Decidable for Probabilistic Automata?. - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001; Filip Mazowiecki; Guillermo A. Pérez 001; James Worrell 001 (ICALP, 2018)

A pseudo-quasi-polynomial algorithm for mean-payoff parity games. - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001 (LICS, 2018)

A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001 (CoRR, 2018)

The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract). - Wojciech Czerwinski; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Filip Mazowiecki (CoRR, 2018)

Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). - Ranko Lazic 001 (FSTTCS, 2019)

Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. - Wojciech Czerwinski; Laure Daviaud; Nathanaël Fijalkow; Marcin Jurdzinski; Ranko Lazic 001; Pawel Parys (SODA, 2019)

The reachability problem for Petri nets is not elementary. - Wojciech Czerwinski; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Filip Mazowiecki (STOC, 2019)

Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems. - Lorenzo Clemente; Slawomir Lasota 001; Ranko Lazic 001; Filip Mazowiecki (ACM Trans. Comput. Log., 2019)

Reachability in Fixed Dimension Vector Addition Systems with States. - Wojciech Czerwinski; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Filip Mazowiecki (CONCUR, 2020)

KReach: A Tool for Reachability in Petri Nets. - Alex Dixon; Ranko Lazic 001 (TACAS (1), 2020)

Verification column. - Ranko Lazic 001 (ACM SIGLOG News, 2020)

Leafy automata for higher-order concurrency. - Alex Dixon; Ranko Lazic 001; Andrzej S. Murawski; Igor Walukiewicz (FoSSaCS, 2021)

Verifying higher-order concurrency with data automata. - Alex Dixon; Ranko Lazic 001; Andrzej S. Murawski; Igor Walukiewicz (LICS, 2021)

A lower bound for the coverability problem in acyclic pushdown VAS. - Matthias Englert; Piotr Hofman; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Juliusz Straszynski (Inf. Process. Lett., 2021)

The Reachability Problem for Two-Dimensional Vector Addition Systems with States. - Michael Blondin; Matthias Englert; Alain Finkel; Stefan Göller; Christoph Haase; Ranko Lazic 001; Pierre McKenzie; Patrick Totzke (J. ACM, 2021)

When are emptiness and containment decidable for probabilistic automata? - Laure Daviaud; Marcin Jurdzinski; Ranko Lazic 001; Filip Mazowiecki; Guillermo A. Pérez 001; James Worrell 001 (J. Comput. Syst. Sci., 2021)

Adversarial Reprogramming Revisited. - Matthias Englert; Ranko Lazic 001 (NeurIPS, 2022)

Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs. - Dmitry Chistikov 001; Matthias Englert; Ranko Lazic 001 (NeurIPS, 2023)

Implicit Regularization of AdaDelta. - Matthias Englert; Ranko Lazic 001; Avi Semler (Trans. Mach. Learn. Res., 2024)

Variance Dichotomy in Feature Spaces of Facial Recognition Systems is a Weak Defense against Simple Weight Manipulation Attacks. - Matthew Bowditch; Mike Paterson; Matthias Englert; Ranko Lazic 001 (Trans. Mach. Learn. Res., 2025)

Text to Stealthy Adversarial Face Masks. - Ben Lewis; Thomas Moyse; James Parkinson; Elizabeth Telford; Callum Whitfield; Ranko Lazic 001 (Trans. Mach. Learn. Res., 2025)

Benignity of loss landscape with weight decay requires both large overparametrization and initialization. - Etienne Boursier; Matthew Bowditch; Matthias Englert; Ranko Lazic 001 (CoRR, 2025)