Ranko Lazic

ORCID

Publication Activity (10 Years)

Years Active: 1999-2023
Publications (10 Years): 60

Top Venues

Publications

Dmitry Chistikov, Matthias Englert, Ranko Lazic
Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs. CoRR (2023)
Ranko Lazic
Verification Column. ACM SIGLOG News 10 (1) (2023)
Dmitry Chistikov, Matthias Englert, Ranko Lazic
Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs. NeurIPS (2023)
Ranko Lazic
Verification column. ACM SIGLOG News 9 (1) (2022)
Ranko Lazic
Verification Column. ACM SIGLOG News 9 (4) (2022)
Matthias Englert, Ranko Lazic
Adversarial Reprogramming Revisited. NeurIPS (2022)
Matthias Englert, Ranko Lazic
Adversarial Reprogramming Revisited. CoRR (2022)
Ranko Lazic
Verification column. ACM SIGLOG News 8 (3) (2021)
Ranko Lazic
Verification column. ACM SIGLOG News 8 (2) (2021)
Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz
Verifying higher-order concurrency with data automata. LICS (2021)
Ranko Lazic, Sylvain Schmitz
The ideal view on Rackoff's coverability technique. Inf. Comput. 277 (2021)
Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, James Worrell
When are emptiness and containment decidable for probabilistic automata? J. Comput. Syst. Sci. 119 (2021)
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
The Reachability Problem for Petri Nets Is Not Elementary. J. ACM 68 (1) (2021)
Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Juliusz Straszynski
A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett. 167 (2021)
Ranko Lazic
Verification column. ACM SIGLOG News 8 (4) (2021)
Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz
Leafy Automata for Higher-Order Concurrency. CoRR (2021)
Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, Patrick Totzke
The Reachability Problem for Two-Dimensional Vector Addition Systems with States. J. ACM 68 (5) (2021)
Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz
Leafy automata for higher-order concurrency. FoSSaCS (2021)
Ranko Lazic
Verification column. ACM SIGLOG News 7 (3) (2020)
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
Reachability in fixed dimension vector addition systems with states. CoRR (2020)
Alex Dixon, Ranko Lazic
KReach: A Tool for Reachability in Petri Nets. TACAS (1) (2020)
Ranko Lazic
Verification column. ACM SIGLOG News 7 (1) (2020)
Ranko Lazic
Verification column. ACM SIGLOG News 7 (4) (2020)
Ranko Lazic
Verification column. ACM SIGLOG News 7 (2) (2020)
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
Reachability in Fixed Dimension Vector Addition Systems with States. CONCUR (2020)
Wojciech Czerwinski, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdzinski, Ranko Lazic, Pawel Parys
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. SODA (2019)
Ranko Lazic
Verification column. ACM SIGLOG News 6 (4) (2019)
Ranko Lazic
Verification column. ACM SIGLOG News 6 (2) (2019)
Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki
Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems. ACM Trans. Comput. Log. 20 (3) (2019)
Ranko Lazic
Verification Column. ACM SIGLOG News 6 (1) (2019)
Ranko Lazic
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). FSTTCS (2019)
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
The reachability problem for Petri nets is not elementary. STOC (2019)
Ranko Lazic
Verification column. ACM SIGLOG News 5 (2) (2018)
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract). CoRR (2018)
Laure Daviaud, Marcin Jurdzinski, Ranko Lazic
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. CoRR (2018)
Laure Daviaud, Marcin Jurdzinski, Ranko Lazic
A pseudo-quasi-polynomial algorithm for mean-payoff parity games. LICS (2018)
Ranko Lazic
Verification column. ACM SIGLOG News 5 (3) (2018)
Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, James Worrell
When is Containment Decidable for Probabilistic Automata?. ICALP (2018)
Ranko Lazic
Verification column. ACM SIGLOG News 5 (4) (2018)
Wojciech Czerwinski, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdzinski, Ranko Lazic, Pawel Parys
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. CoRR (2018)
Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, James Worrell
When is Containment Decidable for Probabilistic Automata? CoRR (2018)
Ranko Lazic, Patrick Totzke
What Makes Petri Nets Harder to Verify: Stack or Data? Concurrency, Security, and Puzzles (2017)
Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki
Timed pushdown automata and branching vector addition systems. LICS (2017)
Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz
Perfect half space games. LICS (2017)
Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, Grégoire Sutre
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. ICALP (2017)
Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz
Perfect Half Space Games. CoRR (2017)
Marcin Jurdzinski, Ranko Lazic
Succinct progress measures for solving parity games. CoRR (2017)
Marcin Jurdzinski, Ranko Lazic
Succinct progress measures for solving parity games. LICS (2017)
Matthias Englert, Ranko Lazic, Patrick Totzke
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. LICS (2016)
Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, Patrick Totzke
Coverability Trees for Petri Nets with Unordered Data. FoSSaCS (2016)
Matthias Englert, Ranko Lazic, Patrick Totzke
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. CoRR (2016)
Ranko Lazic, Sylvain Schmitz
The Complexity of Coverability in ν-Petri Nets. LICS (2016)
Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. ICALP (2016)
Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. CoRR (2016)
Ranko Lazic, Andrzej S. Murawski
Contextual Approximation and Higher-Order Procedures. FoSSaCS (2016)
Ranko Lazic, Joël Ouaknine, James Worrell
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete. ACM Trans. Comput. Log. 17 (3) (2016)
Ranko Lazic, Sylvain Schmitz
The Ideal View on Rackoff's Coverability Technique. RP (2015)
Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz
Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. ICALP (2) (2015)
Ranko Lazic, Sylvain Schmitz
Nonelementary Complexities for Branching VASS, MELL, and Extensions. ACM Trans. Comput. Log. 16 (3) (2015)
Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz
Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. CoRR (2015)
Ranko Lazic, Sylvain Schmitz
Non-elementary complexities for branching VASS, MELL, and extensions. CSL-LICS (2014)
Ranko Lazic, Sylvain Schmitz
Non-Elementary Complexities for Branching VASS, MELL, and Extensions. CoRR (2014)
Ranko Lazic
The reachability problem for vector addition systems with a stack is not elementary. CoRR (2013)
Ranko Lazic, Joël Ouaknine, James Worrell
Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian. MFCS (2013)
Stéphane Demri, Marcin Jurdzinski, Oded Lachish, Ranko Lazic
The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79 (1) (2013)
Michal Rutkowski, Ranko Lazic, Marcin Jurdzinski
Average-price-per-reward games on hybrid automata with strong resets. Int. J. Softw. Tools Technol. Transf. 13 (6) (2011)
Ranko Lazic
Safety alternating automata on data words. ACM Trans. Comput. Log. 12 (2) (2011)
Marcin Jurdzinski, Ranko Lazic
Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Log. 12 (3) (2011)
Stéphane Demri, Ranko Lazic, Arnaud Sangnier
Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci. 411 (22-24) (2010)
Ranko Lazic
The reachability problem for branching vector addition systems requires doubly-exponential space. Inf. Process. Lett. 110 (17) (2010)
Adam Bakewell, Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic
Data-abstraction refinement: a game semantic approach. Int. J. Softw. Tools Technol. Transf. 12 (5) (2010)
Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski
Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. VMCAI (2009)
Stéphane Demri, Ranko Lazic
LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10 (3) (2009)
Stéphane Demri, Marcin Jurdzinski, Oded Lachish, Ranko Lazic
The Covering and Boundedness Problems for Branching Vector Addition Systems. FSTTCS (2009)
Ranko Lazic
Safety alternating automata on data words CoRR (2008)
Stéphane Demri, Ranko Lazic, Arnaud Sangnier
Model checking memoryful linear-time logics over one-counter automata CoRR (2008)
Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell
Nets with Tokens which Carry Data. Fundam. Informaticae 88 (3) (2008)
Marcin Jurdzinski, Ranko Lazic
Alternating Automata on Data Trees and XPath Satisfiability CoRR (2008)
Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski
Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. FORMATS (2008)
Stéphane Demri, Ranko Lazic, Arnaud Sangnier
Model Checking Freeze LTL over One-Counter Automata. FoSSaCS (2008)
Ranko Lazic, Rajagopal Nagarajan
Guest Editorial. Formal Aspects Comput. 19 (3) (2007)
Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell
Nets with Tokens Which Carry Data. ICATPN (2007)
Marcin Jurdzinski, Ranko Lazic
Alternation-free modal mu-calculus for data trees. LICS (2007)
Stéphane Demri, Ranko Lazic, David Nowak
On the freeze quantifier in Constraint LTL: Decidability and complexity. Inf. Comput. 205 (1) (2007)
Aleksandar S. Dimovski, Ranko Lazic
Compositional software verification based on game semantics and process algebra. Int. J. Softw. Tools Technol. Transf. 9 (1) (2007)
Ranko Lazic
Safely Freezing LTL. FSTTCS (2006)
Aleksandar S. Dimovski, Ranko Lazic
Assume-Guarantee Software Verification Based on Game Semantics. ICFEM (2006)
Stéphane Demri, Ranko Lazic
LTL with the Freeze Quantifier and Register Automata CoRR (2006)
Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic
A Counterexample-Guided Refinement Tool for Open Procedural Programs. SPIN (2006)
Stéphane Demri, Ranko Lazic
LTL with the Freeze Quantifier and Register Automata. LICS (2006)
Ranko Lazic, Rajagopal Nagarajan
Preface. Electron. Notes Theor. Comput. Sci. 145 (2006)
Stéphane Demri, Ranko Lazic, David Nowak
On the freeze quantifier in Constraint LTL: decidability and complexity CoRR (2006)
Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic
Data-Abstraction Refinement: A Game Semantic Approach. SAS (2005)
Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic
Abstraction-refinement for game-based model checking. GALOP@ETAPS (2005)
Stéphane Demri, Ranko Lazic, David Nowak
On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. TIME (2005)
Aleksandar S. Dimovski, Ranko Lazic
Software Model Checking Based on Game Semantics and CSP. Electron. Notes Theor. Comput. Sci. 128 (6) (2005)
Ranko Lazic
Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification. INFINITY (2004)
Ranko Lazic, Thomas Christopher Newcomb, A. W. Roscoe
On Model Checking Data-Independent Systems with Arrays with Whole-Array Operations. 25 Years Communicating Sequential Processes (2004)
Aleksandar S. Dimovski, Ranko Lazic
CSP Representation of Game Semantics for Second-Order Idealized Algol. ICFEM (2004)
Ranko Lazic, Thomas Christopher Newcomb, A. W. Roscoe
On model checking data-independent systems with arrays without reset. Theory Pract. Log. Program. 4 (5-6) (2004)

Ranko Lazic.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ranko Lazic