default search action
Ranko Lazic 0001
Person information
- affiliation: University of Warwick, Coventry, UK
Other persons with the same name
- Ranko Lazic 0002 — University of Surrey, Guildford, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [j37]Ranko Lazic:
Verification Column. ACM SIGLOG News 10(1): 23 (2023) - [c48]Dmitry Chistikov, Matthias Englert, Ranko Lazic:
Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs. NeurIPS 2023 - [i20]Dmitry Chistikov, Matthias Englert, Ranko Lazic:
Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias for Correlated Inputs. CoRR abs/2306.06479 (2023) - 2022
- [j36]Ranko Lazic:
Verification column. ACM SIGLOG News 9(1): 5 (2022) - [j35]Ranko Lazic:
Verification Column. ACM SIGLOG News 9(4): 26 (2022) - [c47]Matthias Englert, Ranko Lazic:
Adversarial Reprogramming Revisited. NeurIPS 2022 - [i19]Matthias Englert, Ranko Lazic:
Adversarial Reprogramming Revisited. CoRR abs/2206.03466 (2022) - 2021
- [j34]Ranko Lazic, Sylvain Schmitz:
The ideal view on Rackoff's coverability technique. Inf. Comput. 277: 104582 (2021) - [j33]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: 106079 (2021) - [j32]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): 7:1-7:28 (2021) - [j31]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): 34:1-34:43 (2021) - [j30]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: 78-96 (2021) - [j29]Ranko Lazic:
Verification column. ACM SIGLOG News 8(2): 3 (2021) - [j28]Ranko Lazic:
Verification column. ACM SIGLOG News 8(3): 5 (2021) - [j27]Ranko Lazic:
Verification column. ACM SIGLOG News 8(4): 3 (2021) - [c46]Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz:
Leafy automata for higher-order concurrency. FoSSaCS 2021: 184-204 - [c45]Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz:
Verifying higher-order concurrency with data automata. LICS 2021: 1-13 - [i18]Alex Dixon, Ranko Lazic, Andrzej S. Murawski, Igor Walukiewicz:
Leafy Automata for Higher-Order Concurrency. CoRR abs/2101.08720 (2021) - 2020
- [j26]Ranko Lazic:
Verification column. ACM SIGLOG News 7(1): 34 (2020) - [j25]Ranko Lazic:
Verification column. ACM SIGLOG News 7(2): 3 (2020) - [j24]Ranko Lazic:
Verification column. ACM SIGLOG News 7(3): 28 (2020) - [j23]Ranko Lazic:
Verification column. ACM SIGLOG News 7(4): 3 (2020) - [c44]Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki:
Reachability in Fixed Dimension Vector Addition Systems with States. CONCUR 2020: 48:1-48:21 - [c43]Alex Dixon, Ranko Lazic:
KReach: A Tool for Reachability in Petri Nets. TACAS (1) 2020: 405-412 - [i17]Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki:
Reachability in fixed dimension vector addition systems with states. CoRR abs/2001.04327 (2020)
2010 – 2019
- 2019
- [j22]Ranko Lazic:
Verification Column. ACM SIGLOG News 6(1): 18 (2019) - [j21]Ranko Lazic:
Verification column. ACM SIGLOG News 6(2): 42 (2019) - [j20]Ranko Lazic:
Verification column. ACM SIGLOG News 6(4): 3 (2019) - [j19]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): 14:1-14:31 (2019) - [c42]Ranko Lazic:
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). FSTTCS 2019: 3:1-3:2 - [c41]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: 2333-2349 - [c40]Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki:
The reachability problem for Petri nets is not elementary. STOC 2019: 24-33 - 2018
- [j18]Ranko Lazic:
Verification column. ACM SIGLOG News 5(2): 36 (2018) - [j17]Ranko Lazic:
Verification column. ACM SIGLOG News 5(3): 66 (2018) - [j16]Ranko Lazic:
Verification column. ACM SIGLOG News 5(4): 25 (2018) - [c39]Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, James Worrell:
When is Containment Decidable for Probabilistic Automata?. ICALP 2018: 121:1-121:14 - [c38]Laure Daviaud, Marcin Jurdzinski, Ranko Lazic:
A pseudo-quasi-polynomial algorithm for mean-payoff parity games. LICS 2018: 325-334 - [i16]Laure Daviaud, Marcin Jurdzinski, Ranko Lazic:
A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. CoRR abs/1803.04756 (2018) - [i15]Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, James Worrell:
When is Containment Decidable for Probabilistic Automata? CoRR abs/1804.09077 (2018) - [i14]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 abs/1807.10546 (2018) - [i13]Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki:
The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract). CoRR abs/1809.07115 (2018) - 2017
- [c37]Ranko Lazic, Patrick Totzke:
What Makes Petri Nets Harder to Verify: Stack or Data? Concurrency, Security, and Puzzles 2017: 144-161 - [c36]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: 119:1-119:14 - [c35]Lorenzo Clemente, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki:
Timed pushdown automata and branching vector addition systems. LICS 2017: 1-12 - [c34]Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz:
Perfect half space games. LICS 2017: 1-11 - [c33]Marcin Jurdzinski, Ranko Lazic:
Succinct progress measures for solving parity games. LICS 2017: 1-9 - [e2]Thomas Gibson-Robinson, Philippa J. Hopcroft, Ranko Lazic:
Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 10160, Springer 2017, ISBN 978-3-319-51045-3 [contents] - [i12]Marcin Jurdzinski, Ranko Lazic:
Succinct progress measures for solving parity games. CoRR abs/1702.05051 (2017) - [i11]Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz:
Perfect Half Space Games. CoRR abs/1704.05626 (2017) - 2016
- [j15]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): 16 (2016) - [c32]Ranko Lazic, Andrzej S. Murawski:
Contextual Approximation and Higher-Order Procedures. FoSSaCS 2016: 162-179 - [c31]Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, Patrick Totzke:
Coverability Trees for Petri Nets with Unordered Data. FoSSaCS 2016: 445-461 - [c30]Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke:
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. ICALP 2016: 105:1-105:13 - [c29]Ranko Lazic, Sylvain Schmitz:
The Complexity of Coverability in ν-Petri Nets. LICS 2016: 467-476 - [c28]Matthias Englert, Ranko Lazic, Patrick Totzke:
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. LICS 2016: 477-484 - [i10]Matthias Englert, Ranko Lazic, Patrick Totzke:
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. CoRR abs/1602.00477 (2016) - [i9]Stefan Göller, Christoph Haase, Ranko Lazic, Patrick Totzke:
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. CoRR abs/1602.05547 (2016) - 2015
- [j14]Ranko Lazic, Sylvain Schmitz:
Nonelementary Complexities for Branching VASS, MELL, and Extensions. ACM Trans. Comput. Log. 16(3): 20:1-20:30 (2015) - [c27]Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz:
Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. ICALP (2) 2015: 260-272 - [c26]Ranko Lazic, Sylvain Schmitz:
The Ideal View on Rackoff's Coverability Technique. RP 2015: 76-88 - [i8]Marcin Jurdzinski, Ranko Lazic, Sylvain Schmitz:
Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. CoRR abs/1502.06875 (2015) - 2014
- [c25]Ranko Lazic, Sylvain Schmitz:
Non-elementary complexities for branching VASS, MELL, and extensions. CSL-LICS 2014: 61:1-61:10 - [i7]Ranko Lazic, Sylvain Schmitz:
Non-Elementary Complexities for Branching VASS, MELL, and Extensions. CoRR abs/1401.6785 (2014) - 2013
- [j13]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): 23-38 (2013) - [c24]Ranko Lazic, Joël Ouaknine, James Worrell:
Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian. MFCS 2013: 643-654 - [i6]Ranko Lazic:
The reachability problem for vector addition systems with a stack is not elementary. CoRR abs/1310.1767 (2013) - 2011
- [j12]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): 553-569 (2011) - [j11]Ranko Lazic:
Safety alternating automata on data words. ACM Trans. Comput. Log. 12(2): 10:1-10:24 (2011) - [j10]Marcin Jurdzinski, Ranko Lazic:
Alternating automata on data trees and XPath satisfiability. ACM Trans. Comput. Log. 12(3): 19:1-19:21 (2011) - 2010
- [j9]Ranko Lazic:
The reachability problem for branching vector addition systems requires doubly-exponential space. Inf. Process. Lett. 110(17): 740-745 (2010) - [j8]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): 373-389 (2010) - [j7]Stéphane Demri, Ranko Lazic, Arnaud Sangnier:
Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci. 411(22-24): 2298-2316 (2010)
2000 – 2009
- 2009
- [j6]Stéphane Demri, Ranko Lazic:
LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3): 16:1-16:30 (2009) - [c23]Stéphane Demri, Marcin Jurdzinski, Oded Lachish, Ranko Lazic:
The Covering and Boundedness Problems for Branching Vector Addition Systems. FSTTCS 2009: 181-192 - [c22]Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski:
Average-Price-per-Reward Games on Hybrid Automata with Strong Resets. VMCAI 2009: 167-181 - 2008
- [j5]Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell:
Nets with Tokens which Carry Data. Fundam. Informaticae 88(3): 251-274 (2008) - [c21]Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, Michal Rutkowski:
Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. FORMATS 2008: 63-77 - [c20]Stéphane Demri, Ranko Lazic, Arnaud Sangnier:
Model Checking Freeze LTL over One-Counter Automata. FoSSaCS 2008: 490-504 - [i5]Ranko Lazic:
Safety alternating automata on data words. CoRR abs/0802.4237 (2008) - [i4]Marcin Jurdzinski, Ranko Lazic:
Alternating Automata on Data Trees and XPath Satisfiability. CoRR abs/0805.0330 (2008) - [i3]Stéphane Demri, Ranko Lazic, Arnaud Sangnier:
Model checking memoryful linear-time logics over one-counter automata. CoRR abs/0810.5517 (2008) - 2007
- [j4]Ranko Lazic, Rajagopal Nagarajan:
Guest Editorial. Formal Aspects Comput. 19(3): 275 (2007) - [j3]Stéphane Demri, Ranko Lazic, David Nowak:
On the freeze quantifier in Constraint LTL: Decidability and complexity. Inf. Comput. 205(1): 2-24 (2007) - [j2]Aleksandar S. Dimovski, Ranko Lazic:
Compositional software verification based on game semantics and process algebra. Int. J. Softw. Tools Technol. Transf. 9(1): 37-51 (2007) - [c19]Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell:
Nets with Tokens Which Carry Data. ICATPN 2007: 301-320 - [c18]Marcin Jurdzinski, Ranko Lazic:
Alternation-free modal mu-calculus for data trees. LICS 2007: 131-140 - 2006
- [c17]Ranko Lazic:
Safely Freezing LTL. FSTTCS 2006: 381-392 - [c16]Aleksandar S. Dimovski, Ranko Lazic:
Assume-Guarantee Software Verification Based on Game Semantics. ICFEM 2006: 529-548 - [c15]Stéphane Demri, Ranko Lazic:
LTL with the Freeze Quantifier and Register Automata. LICS 2006: 17-26 - [c14]Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic:
A Counterexample-Guided Refinement Tool for Open Procedural Programs. SPIN 2006: 288-292 - [e1]Ranko Lazic, Rajagopal Nagarajan:
Proceedings of the 5th International Workshop on Automated Verification of Critical Systems, AVoCS 2005, University of Warwick, UK, September 12-13, 2005. Electronic Notes in Theoretical Computer Science 145, Elsevier 2006 [contents] - [i2]Stéphane Demri, Ranko Lazic, David Nowak:
On the freeze quantifier in Constraint LTL: decidability and complexity. CoRR abs/cs/0609008 (2006) - [i1]Stéphane Demri, Ranko Lazic:
LTL with the Freeze Quantifier and Register Automata. CoRR abs/cs/0610027 (2006) - 2005
- [c13]Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic:
Abstraction-refinement for game-based model checking. GALOP@ETAPS 2005: 139 - [c12]Aleksandar S. Dimovski, Dan R. Ghica, Ranko Lazic:
Data-Abstraction Refinement: A Game Semantic Approach. SAS 2005: 102-117 - [c11]Stéphane Demri, Ranko Lazic, David Nowak:
On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. TIME 2005: 113-121 - [c10]Ranko Lazic, Rajagopal Nagarajan:
Preface. AVoCS 2005: 1-2 - 2004
- [j1]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): 659-693 (2004) - [c9]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: 275-291 - [c8]Aleksandar S. Dimovski, Ranko Lazic:
CSP Representation of Game Semantics for Second-Order Idealized Algol. ICFEM 2004: 146-161 - [c7]Xu Wang, A. W. Roscoe, Ranko Lazic:
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. IFM 2004: 247-266 - [c6]Ranko Lazic:
Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification. INFINITY 2004: 3-19 - [c5]Ranko Lazic, Thomas Christopher Newcomb, Bill Roscoe:
Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting. INFINITY 2004: 61-86 - [c4]Aleksandar S. Dimovski, Ranko Lazic:
Software Model Checking Based on Game Semantics and CSP. AVoCS 2004: 105-125 - 2003
- [c3]Ranko Lazic, David Nowak:
On a Semantic Definition of Data Independence . TLCA 2003: 226-240 - 2000
- [c2]Ranko Lazic, David Nowak:
A Unifying Approach to Data-Independence. CONCUR 2000: 581-595
1990 – 1999
- 1999
- [b1]Ranko S. Lazic:
A semantic study of data independence with applications to model checking. University of Oxford, UK, 1999 - [c1]Ranko Lazic, Bill Roscoe:
Data Independence with Generalised Predicate Symbols. PDPTA 1999: 319-326
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 21:19 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint