2022

Englert, Matthias and Lazic, Ranko (2022) Adversarial reprogramming revisited. In: Thirty-sixth Conference on Neural Information Processing Systems (NeurIPS 2022), New Orleans, 28 Nov - 09 Dec 2022. Published in: Advances in Neural Information Processing Systems (NeurIPS 2022), 35 pp. 28588-28600.

2021

Blondin, Michael, Englert, Matthias, Finkel, Alain, Göller, Stefan , Haase, Christoph, Lazic, Ranko, McKenzie, Pierre and Totzke, Patrick (2021) The reachability problem for two-dimensional vector addition systems with states. Journal of the ACM, 68 (5). pp. 1-43. 34. doi:10.1145/3464794 ISSN 0004-5411.

Daviaud, Laure, Jurdzinski, Marcin, Lazic, Ranko, Mazowiecki, Filip, Pérez, Guillermo A. and Worrell, James (2021) When are emptiness and containment decidable for probabilistic automata? Journal of Computer and System Sciences, 119 . pp. 78-96. doi:10.1016/j.jcss.2021.01.006 ISSN 0022-0000.

Dixon, Alex, Lazic, Ranko, Murawski, Andrzej S. and Walukiewicz, Igor (2021) Verifying higher-order concurrency with data automata. In: ACM/IEEE LICS 2021 : 36th Annual Symposium on Logic in Computer Science, Virtual conference, 29 Jun - 2 Jul 2021. Published in: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ISBN 9781665448963. doi:10.1109/LICS52264.2021.9470691

Lazic, Ranko and Schmitz, Sylvain (2021) The ideal view on Rackoff's coverability technique. Information and Computation, 277 . 104582. doi:10.1016/j.ic.2020.104582 ISSN 0890-5401.

Englert, Matthias, Hofman, Piotr, Lasota, Sławomir, Lazic, Ranko, Leroux, Jérôme and Straszyński, Juliusz (2021) A lower bound for the coverability problem in acyclic pushdown VAS. Information Processing Letters, 167 . 106079. doi:10.1016/j.ipl.2020.106079 ISSN 0020-0190.

Dixon, Alex, Lazic, Ranko, Murawski, Andrzej S. and Walukiewicz, Igor (2021) Leafy automata for higher-order concurrency. In: FoSSaCS 21 , Virtual conference, 27 Mar-1 Apr 2021. Published in: FOSSACS 2021: Foundations of Software Science and Computation Structures , 12650 pp. 184-204. ISBN 9783030719944. doi:10.1007/978-3-030-71995-1_10

Czerwinski, Wojciech, Lasota, Slawomir , Lazic, Ranko, Leroux, Jérôme and Mazowiecki, Filip (2021) The reachability problem for petri nets is not elementary. Journal of the ACM, 68 (1). 7. doi:10.1145/3422822 ISSN 0004-5411.

2020

Czerwiński, Wojciech, Lasota, Slawomir, Lazic, Ranko, Leroux, Jerome and Mazowiecki, Filip (2020) Reachability in fixed dimension vector addition systems with states. In: 31st International Conference on Concurrency Theory (CONCUR 2020), Virtual conference, 01-04 Sep 2020. Published in: Leibniz International Proceedings in Informatics (LIPIcs), 171 doi:10.4230/LIPIcs.CONCUR.2020.48 ISSN 1868-8969.

2019

Lazic, Ranko (2019) Finkel was right : counter-examples to several conjectures on variants of vector addition systems (invited talk). In: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), Bombay, India, 11-13 Dec 2019. Published in: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), 150 3:1-3:2. ISBN 9783959771313. doi:10.4230/LIPIcs.FSTTCS.2019.3 ISSN 1868-8969.

Czerwiński, Wojciech, Lasota, Sławomir, Lazic, Ranko, Leroux, Jerome and Mazowiecki, Filip (2019) The reachability problem for Petri nets is not elementary. In: STOC 2019, Phoenix, AZ, USA, 23-26 Jun 2019. Published in: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing pp. 24-33. ISBN 9781450367059. doi:10.1145/3313276.3316369

Clemente, Lorenzo, Lasota, Sławomir, Lazic, Ranko and Mazowiecki, Filip (2019) Binary reachability of timed-register pushdown automata and branching vector addition systems. ACM Transactions on Computational Logic, 20 (3). pp. 1-31. 14. doi:10.1145/3326161 ISSN 1529-3785.

Dixon, Alex and Lazic, Ranko (2019) KReach : a tool for reachability in petri nets. In: TACAS 2020 : 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, 25-30 Apr 2020. Published in: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. , 12078 pp. 405-412. ISBN 9783030451899. doi:10.1007/978-3-030-45190-5_22

Czerwiński, Wojciech, Daviaud, Laure, Fijalkow, Nathanael, Jurdzinski, Marcin, Lazic, Ranko and Parys, Pawel (2019) Universal trees grow inside separating automata : quasi-polynomial lower bounds for parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA 2019), California, 6-9 Jan 2019. Published in: Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms pp. 2333-2349. ISBN 9781611975482. doi:10.1137/1.9781611975482.142

2018

Daviaud, Laure, Jurdzinski, Marcin, Lazic, Ranko, Mazowiecki, Filip, Pérez, Guillermo A. and Worell, James (2018) When is containment decidable for probabilistic automata? In: ICALP 2018: 45th International Colloquium on Automata, Languages, and Programming, Prague, Czech Republic, 9-13 Jul 2018. Published in: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), 107 121:1-121:14. ISBN 9783959770767. doi:10.4230/LIPIcs.ICALP.2018.121

Daviaud, Laure, Jurdzinski, Marcin and Lazic, Ranko (2018) A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Oxford, 9–12 Jul 2018. Published in: LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science pp. 325-334. ISBN 9781450355834. doi:10.1145/3209108.3209162

2017

Colcombet, Thomas , Jurdzinski, Marcin, Lazic, Ranko and Schmitz, Sylvain (2017) Perfect half space games. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 20-23 Jun 2017. Published in: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ISBN 9781509030187. doi:10.1109/LICS.2017.8005105

Figueira, Diego, Lazic, Ranko, Leroux, Jerome, Mazowiecki, Filip and Sutre, Grégoire (2017) Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In: The 44th International Colloquium on Automata, Languages, and Programming (ICALP), Warsaw, Poland, 10-14 Jul 2017. Published in: 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), 80 119 : 1-119: 14. ISBN 9783959770415. doi:10.4230/LIPIcs.ICALP.2017.119 ISSN 1868-8969.

Clemente, Lorenzo, Lasota, Slawomir, Lazic, Ranko and Mazowiecki, Filip (2017) Timed pushdown automata and branching vector addition systems. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 20-23 Jun 2017. Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ISBN 9781509030194. doi:10.1109/LICS.2017.8005083

Lazic, Ranko and Totzke, Patrick (2017) What makes petri nets harder to verify : stack or data?, Concurrency, security, and puzzles : Festschrift for A.W. Roscoe on the occasion of his 60th birthday. In: Concurrency, Security, and Puzzles : Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, 10160 . Springer, pp. 144-161. ISBN 9783319510453

Jurdzinski, Marcin and Lazic, Ranko (2017) Succinct progress measures for solving parity games. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, 20-23 Jun 2017. Published in: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) pp. 1-9. ISBN 9781509030187. doi:10.1109/LICS.2017.8005092

2016

Lazic, Ranko and Schmitz, Sylvain (2016) The complexity of coverability in ν-Petri nets. In: 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), New York City, USA, 5–8 Jul 2016. Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) pp. 467-476. ISBN 9781450343916. doi:10.1145/2933575.2933593

Goller, Stefan, Haase, Christoph, Lazic, Ranko and Totzke, Patrick (2016) A polynomial-time algorithm for reachability in branching VASS in dimension one. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), Rome, Italy, 12-15 Jul 2016. Published in: Leibniz International Proceedings in Informatics (LIPIcs) ISBN 9783959770132. doi:10.4230/LIPIcs.ICALP.2016.105 ISSN 1868-8969.

Englert, Matthias, Lazic, Ranko and Totzke, Patrick (2016) Reachability in two-dimensional unary vector addition systems with states is NL-complete. In: Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), New York City, USA, 5–8 Jul 2016. Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Hofman, Piotr , Lasota, Slawomir , Lazic, Ranko, Leroux, Jerome , Schmitz, Sylvain and Totzke, Patrick (2016) Coverability trees for petri nets with unordered data. In: 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Eindhoven, The Netherlands, 2-8 Apr 2016. Published in: Lecture Notes in Computer Science, 9634 pp. 445-461. ISBN 9783662496299. doi:10.1007/978-3-662-49630-5_26 ISSN 0302-9743.

Lazic, Ranko, Ouaknine, Joel and Worrell, James (2016) Zeno, Hercules, and the Hydra : safety metric temporal logic is ACKERMANN-complete. ACM Transactions on Computational Logic, 17 (3). 16. doi:10.1145/2874774 ISSN 1557-945X .

Lazic, Ranko and Murawski, Andrzej S. (2016) Contextual approximation and higher-order procedures. In: 19th International Conference, FOSSACS 2016, Eindhoven, The Netherlands, 2-8 Apr 2016. Published in: Foundations of Software Science and Computation Structures :19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceeding, 9634 pp. 162-179. ISBN 9783662496299. doi:10.1007/978-3-662-49630-5_10 ISSN 0302-9743.

2015

Lazic, Ranko and Schmitz, Sylvain (2015) The ideal view on Rackoff's coverability technique. In: 9th International Workshop on Reachability Problems, Warsaw, Poland, 21-23 Sep 2015. Published in: Reachability Problems : 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings, 9328 pp. 76-88. doi:10.1007/978-3-319-24537-9_8 ISSN 0302-9743.

Jurdzinski, Marcin, Lazic, Ranko and Schmitz, Sylvain (2015) Fixed-dimensional energy games are in pseudo-polynomial time. In: 42nd International Colloquium, ICALP 2015, Kyoto, Japan, 6-10 Jul 2015. Published in: Automata, Languages, and Programming : 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, 9135 pp. 260-272. ISBN 9783662476659. doi:10.1007/978-3-662-47666-6_21 ISSN 0302-9743.

Lazic, Ranko and Schmitz, Sylvain (2015) Nonelementary complexities for branching VASS, MELL, and extensions. ACM Transactions on Computational Logic (TOCL), Volume 16 (Number 3). Article number 20. doi:10.1145/2733375 ISSN 1529-3785.

2014

Lazic, Ranko and Schmitz, Sylvain (2014) Non-elementary complexities for branching VASS, MELL, and extensions. In: Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th ACM/IEEE Symposium on Logic in Computer Science, Vienna, Austria, 14-18 Jul 2014. Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Article number 61). ISBN 9781450328869. doi:10.1145/2603088.2603129

2013

Demri, Stéphane P., Jurdzinski, Marcin, Lachish, Oded and Lazic, Ranko (2013) The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 79 (1). pp. 23-38. doi:10.1016/j.jcss.2012.04.002 ISSN 0022-0000.

2011

Jurdzinski, Marcin and Lazic, Ranko (2011) Alternating automata on data trees and XPath satisfiability. ACM Transactions on Computational Logic (TOCL), Volume 12 (Number 3). pp. 1-21. doi:10.1145/1929954.1929956 ISSN 1529-3785.

Lazic, Ranko (2011) Safety alternating automata on data words. ACM Transactions on Computational Logic (TOCL), Vol.12 (No.2). pp. 1-24. doi:10.1145/1877714.1877716 ISSN 1529-3785.

2010

Bakewell, Adam, Dimovski, Aleksandar, Ghica, Dan R. and Lazic, Ranko (2010) Data-abstraction refinement : a game semantic approach. International Journal on Software Tools for Technology Transfer, Vol.12 (No.5). pp. 373-389. doi:10.1007/s10009-010-0143-0 ISSN 1433-2779.

Lazic, Ranko (2010) The reachability problem for branching vector addition systems requires doubly-exponential space. Information Processing Letters, Vol.110 (No.17). pp. 740-745. doi:10.1016/j.ipl.2010.06.008 ISSN 0020-0190.

Demri, Stéphane P., Lazic, Ranko and Sangnier, Arnaud (2010) Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science, Vol.411 (No.22-24). pp. 2298-2316. doi:10.1016/j.tcs.2010.02.021 ISSN 0304-3975.

2009

Demri, Stéphane P. and Lazic, Ranko (2009) LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic (TOCL), Vol.10 (No.3). p. 16. doi:10.1145/1507244.1507246 ISSN 1529-3785.

Lazic, Ranko, Jurdzinski, Marcin and Rutkowski, Michał, Ph.D. (2009) Average-price-per-reward games on hybrid automata with strong resets. In: Jones, Neil D. and Müller-Olm, Markus, (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science (5403). London: Springer, pp. 167-181. ISBN 9783540938996

2008

Bouyer, Patricia, Brihaye, Thomas, Jurdzinski, Marcin, Lazic, Ranko and Rutkowski, Michał, Ph.D. (2008) Average-price and reachability-price games on hybrid automata with strong resets. In: 6th International Conference on Formal Modeling and Analysis of Timed Systems, St Malo, France, 15-17 September, 2008. Published in: Lecture Notes in Computer Science, 5215 pp. 63-77. ISBN 9783540857778. doi:10.1007/978-3-540-85778-5_6 ISSN 0302-9743.

Lazic, Ranko, Newcomb, Tom, Ouaknine, Joel, Roscoe, A. W. and Worrell, James (2008) Nets with tokens which carry data. Fundamenta Informaticae, Vol.88 (No.3). pp. 251-274. ISSN 0169-2968.

2007

Jurdzinski, Marcin and Lazic, Ranko (2007) Alternation-free modal mu-calculus for data trees. In: 22nd Annual IEEE Symposium on Logic in Computer Science , Wroclaw, Poland, 10-14 Jul 2007. Published in: 22nd Annual IEEE Symposium on Logic in Computer Science : proceedings : Wroc¿aw, Poland, 10-14 July, 2007 pp. 131-140. ISBN 9780769529080. ISSN 1043-6871.

Lazic, Ranko, Newcomb, Tom, Ouaknine, Joel, Roscoe, A. W. and Worrell, James (2007) Nets with tokens which carry data. In: Kleijnen, J. and Yakovlev, A., (eds.) Petri Nets and Other Models of Concurrency – ICATPN 2007 : 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007. Proceedings. Lecture Notes in Computer Science, Volume 4546 . Heidelberg : Springer Verlag, pp. 301-320. ISBN 9783540730934

2006

Dimovski, Aleksandar and Lazic, Ranko (2006) Assume-guarantee software verification based on game semantics. In: 8th International Conference on Formal Engineering Methods (ICFEM 2006), Macao, China, 01-03 Nov 2006. Published in: Formal Methods and Software Engineering, Proceedings, Volume 4260 pp. 529-548. ISBN 3-540-47460-9. ISSN 0302-9743.

Lazic, Ranko (2006) Safely freezing LTL. In: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, Calcutta, India, 13-15 Dec 2006, Volume 4337 pp. 381-392. ISBN 9783540499947. ISSN 0302-9743.

2005

Demri, Stephane, Lazic, Ranko and Nowak, David (2005) On the freeze quantifier in Constraint LTL : decidability and complexity. In: 12th International Symposium on Temporal Representation and Reasoning, Burlington, VT, 23-25 Jun 2005. Published in: Information and Computation, Volume 205 (Number 1). pp. 2-24. doi:10.1016/j.ic.2006.08.003 ISSN 0890-5401.

Lazic, Ranko, Newcomb, Tom and Roscoe, A. W. (2005) On model checking data-independent systems with arrays with whole-array operations. In: Abadallah, A. E. and Jones, C. B. and Sanders, J. W., (eds.) Communicating Sequential Processes. The First 25 Years. Lecture Notes in Computer Science, Volume 3525 . Springer Berlin Heidelberg, pp. 275-291. ISBN 9783540258131

2004

Dimovski, Aleksandar and Lazic, Ranko (2004) CSP representation of game semantics for second-order idealized Algol. In: Davies, J. and Schulte, W. and Barnett, M., (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, Volume 3308 . Springer Berlin Heidelberg, pp. 146-161. ISBN 9783540238416

Dimovski, Aleksandar and Lazic, Ranko (2004) CSP representation of game semantics for second-order idealized Algol. University of Warwick. Department of Computer Science. (Department of Computer Science research report).

Lazic, Ranko, Newcomb, Tom and Roscoe, A. W. (2004) On model checking data-independent systems with arrays with whole-array operations. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)

Lazic, Ranko, Newcomb, Tom and Roscoe, A. W. (2004) Polymorphic systems with arrays : decidability and undecidability. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)

Dimovski, Aleksandar and Lazic, Ranko (2004) Software model checking based on game semantics and CSP. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)

2003

Lazic, Ranko and Nowak, David (2003) On a semantic definition of data independence. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)