Jérôme Leroux

121 papers A* 19A 5B 24C 2Journal 45Unranked 24
YearRankTypeTitle / Venue / Authors
2026 B conf
Bridging the Gap Between Plain VASS and Branching VASS.
FoSSaCS
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
2026 J jnl
Reachability in VASS Extended with Integer Counters.
CoRR
Clotilde Bizière, Wojciech Czerwinski, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Lukasz Orlikowski, Antoni Puch, Henry Sinclair-Banks
2025 B conf
On the Reachability Problem for Two-Dimensional Branching VASS.
MFCS
Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, Grégoire Sutre
2025 J jnl
On the Reachability Problem for Two-Dimensional Branching VASS.
CoRR
Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, Grégoire Sutre
2025 J jnl
Preface to special issue MFCS 2023.
Inf. Comput.
Jérôme Leroux, David Peleg
2025 B conf
Structural Liveness of Conservative Petri Nets.
FoSSaCS
Petr Jancar, Jérôme Leroux, Jiri Valusek
2025 J jnl
Structural Liveness of Conservative Petri Nets.
CoRR
Petr Jancar, Jérôme Leroux, Jiri Valusek
2024 — conf
A State-of-the-Art Karp-Miller Algorithm Certified in Coq.
TACAS (1)
Thibault Hilaire, David Ilcinkas, Jérôme Leroux
2024 — conf
Ackermannian Completion of Separators.
FoSSaCS (1)
Jérôme Leroux
2024 B conf
Invariants for One-Counter Automata with Disequality Tests.
CONCUR
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, Nicolas Waldburger
2024 J jnl
Invariants for One-Counter Automata with Disequality Tests.
CoRR
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, Nicolas Waldburger
2024 J jnl
On the Home-Space Problem for Petri Nets and its Ackermannian Complexity.
Log. Methods Comput. Sci.
Petr Jancar, Jérôme Leroux
2024 — conf
On the Home-Space Problem for Petri Nets.
Taming the Infinities of Concurrency
Petr Jancar, Jérôme Leroux
2023 B ed.
48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, Bordeaux, France, August 28 - September 1, 2023
MFCS
Jérôme Leroux, Sylvain Lombardy, David Peleg
2023 J jnl
Lower bounds on the state complexity of population protocols.
Distributed Comput.
Philipp Czerner, Javier Esparza, Jérôme Leroux
2023 — conf
New Lower Bounds for Reachability in Vector Addition Systems.
FSTTCS
Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, Lukasz Orlikowski
2023 J jnl
New Lower Bounds for Reachability in Vector Addition Systems.
CoRR
Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, Lukasz Orlikowski
2023 B conf
The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets.
CONCUR
Petr Jancar, Jérôme Leroux
2022 J jnl
Compiling Petri Net Mutual Reachability in Presburger.
CoRR
Jérôme Leroux
2022 J jnl
Semilinear Home-space is Decidable for Petri Nets.
CoRR
Petr Jancar, Jérôme Leroux
2022 A* conf
State Complexity of Protocols with Leaders.
PODC
Jérôme Leroux
2021 J jnl
A lower bound for the coverability problem in acyclic pushdown VAS.
Inf. Process. Lett.
Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Juliusz Straszynski
2021 B conf
Flat Petri Nets (Invited Talk).
Petri Nets
Jérôme Leroux
2021 — conf
New Algorithms for Combinations of Objectives using Separating Automata.
GandALF
Ashwani Anand, Nathanaël Fijalkow, Aliénor Goubault-Larrecq, Jérôme Leroux, Pierre Ohlmann
2021 J jnl
State Complexity of Counting Population Protocols With Leaders.
CoRR
Jérôme Leroux
2021 J jnl
The Reachability Problem for Petri Nets Is Not Elementary.
J. ACM
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
2021 A* conf
The Reachability Problem for Petri Nets is Not Primitive Recursive.
FOCS
Jérôme Leroux
2021 J jnl
The Reachability Problem for Petri Nets is Not Primitive Recursive.
CoRR
Jérôme Leroux
2020 A* conf
Efficient Analysis of VASS Termination Complexity.
LICS
Antonín Kucera, Jérôme Leroux, Dominik Velan
2020 B conf
Reachability in Fixed Dimension Vector Addition Systems with States.
CONCUR
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
2020 B conf
Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free.
CONCUR
Jérôme Leroux, Grégoire Sutre
2020 J jnl
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free.
CoRR
Jérôme Leroux, Grégoire Sutre
2020 J jnl
Reachability in fixed dimension vector addition systems with states.
CoRR
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
2020 A* conf
When Reachability Meets Grzegorczyk.
LICS
Jérôme Leroux
2019 J jnl
Co-Finiteness and Co-Emptiness of Reachability Sets in Vector Addition Systems with States.
Fundam. Informaticae
Petr Jancar, Jérôme Leroux, Grégoire Sutre
2019 — conf
Distance Between Mutually Reachable Petri Net Configurations.
FSTTCS
Jérôme Leroux
2019 J jnl
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems.
CoRR
Jérôme Leroux, M. Praveen, Philippe Schnoebelen, Grégoire Sutre
2019 J jnl
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems.
Log. Methods Comput. Sci.
Jérôme Leroux, M. Praveen, Philippe Schnoebelen, Grégoire Sutre
2019 B conf
Petri Net Reachability Problem (Invited Talk).
MFCS
Jérôme Leroux
2019 — ed.
Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2-3rd September 2019.
GandALF
Jérôme Leroux, Jean-François Raskin
2019 A* conf
Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension.
LICS
Jérôme Leroux, Sylvain Schmitz
2019 J jnl
Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension.
CoRR
Jérôme Leroux, Sylvain Schmitz
2019 A* conf
The reachability problem for Petri nets is not elementary.
STOC
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
2018 B conf
Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States.
Petri Nets
Petr Jancar, Jérôme Leroux, Grégoire Sutre
2018 J jnl
Occam's Razor applied to the Petri net coverability problem.
Theor. Comput. Sci.
Thomas Geffroy, Jérôme Leroux, Grégoire Sutre
2018 A* conf
Polynomial Vector Addition Systems With States.
ICALP
Jérôme Leroux
2018 — conf
Reachability for Two-Counter Machines with One Test and One Reset.
FSTTCS
Alain Finkel, Jérôme Leroux, Grégoire Sutre
2018 J jnl
The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract).
CoRR
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki
2017 — conf
Backward coverability with pruning for lossy channel systems.
SPIN
Thomas Geffroy, Jérôme Leroux, Grégoire Sutre
2017 A* conf
Linear combinations of unordered data vectors.
LICS
Piotr Hofman, Jérôme Leroux, Patrick Totzke
2017 A* conf
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One.
ICALP
Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, Grégoire Sutre
2017 J jnl
Verification of population protocols.
Acta Informatica
Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar
2016 B conf
Coverability Trees for Petri Nets with Unordered Data.
FoSSaCS
Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, Patrick Totzke
2016 J jnl
Guiding Craig interpolation with domain-specific abstractions.
Acta Informatica
Jérôme Leroux, Philipp Rümmer, Pavle Subotic
2016 A conf
Ideal Decompositions for Vector Addition Systems (Invited Talk).
STACS
Jérôme Leroux, Sylvain Schmitz
2016 J jnl
Linear Combinations of Unordered Data Vectors.
CoRR
Piotr Hofman, Jérôme Leroux, Patrick Totzke
2016 — conf
Model Checking Population Protocols.
FSTTCS
Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar
2016 — conf
Occam's Razor Applied to the Petri Net Coverability Problem.
RP
Thomas Geffroy, Jérôme Leroux, Grégoire Sutre
2016 J jnl
Occam's Razor Applied to the Petri Net Coverability Problem.
CoRR
Thomas Geffroy, Jérôme Leroux, Grégoire Sutre
2016 J jnl
Preface.
Fundam. Informaticae
Parosh Aziz Abdulla, Stéphane Demri, Alain Finkel, Jérôme Leroux, Igor Potapov
2015 A* conf
Demystifying Reachability in Vector Addition Systems.
LICS
Jérôme Leroux, Sylvain Schmitz
2015 — conf
On Boundedness Problems for Pushdown Vector Addition Systems.
RP
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
2015 J jnl
On Boundedness Problems for Pushdown Vector Addition Systems.
CoRR
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
2015 — conf
On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension.
ICALP (2)
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
2015 J jnl
On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension.
CoRR
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
2015 J jnl
Reachability in Vector Addition Systems Demystified.
CoRR
Jérôme Leroux, Sylvain Schmitz
2015 J jnl
Recent and simple algorithms for Petri nets.
Softw. Syst. Model.
Alain Finkel, Jérôme Leroux
2015 J jnl
Structurally Cyclic Petri Nets.
Log. Methods Comput. Sci.
Frank Drewes, Jérôme Leroux
2015 B conf
Verification of Population Protocols.
CONCUR
Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar
2014 — conf
Hyper-Ackermannian bounds for pushdown vector addition systems.
CSL-LICS
Jérôme Leroux, M. Praveen, Grégoire Sutre
2014 J jnl
Neue, einfache Algorithmen für Petrinetze.
Inform. Spektrum
Alain Finkel, Jérôme Leroux
2014 — conf
On Functions Weakly Computable by Petri Nets and Vector Addition Systems.
RP
Jérôme Leroux, Philippe Schnoebelen
2014 B conf
The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems.
ATVA
Jérôme Leroux, Vincent Penelle, Grégoire Sutre
2013 B conf
A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness.
CONCUR
Jérôme Leroux, M. Praveen, Grégoire Sutre
2013 — conf
Acceleration For Presburger Petri Nets.
VPT@CAV
Jérôme Leroux
2013 B conf
Acceleration for Petri Nets.
ATVA
Jérôme Leroux
2013 A* conf
On the Context-Freeness Problem for Vector Addition Systems.
LICS
Jérôme Leroux, Vincent Penelle, Grégoire Sutre
2013 A* conf
Presburger Vector Addition Systems.
LICS
Jérôme Leroux
2013 J jnl
Vector Addition System Reversible Reachability Problem
Log. Methods Comput. Sci.
Jérôme Leroux
2012 J jnl
Model Checking Vector Addition Systems with one zero-test
Log. Methods Comput. Sci.
Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun
2012 J jnl
Reachability Analysis of Communicating Pushdown Systems
Log. Methods Comput. Sci.
Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre
2012 — ed.
Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings
RP
Alain Finkel, Jérôme Leroux, Igor Potapov
2012 — conf
Vector Addition Systems Reachability Problem (A Simpler Solution).
Turing-100
Jérôme Leroux
2011 A* conf
The BINCOA Framework for Binary Code Analysis.
CAV
Sébastien Bardin, Philippe Herrmann, Jérôme Leroux, Olivier Ly, Renaud Tabary, Aymeric Vincent
2011 C conf
Vector Addition System Reachability Problem: A Short Self-contained Proof.
LATA
Jérôme Leroux
2011 B conf
Vector Addition System Reversible Reachability Problem.
CONCUR
Jérôme Leroux
2011 A* conf
Vector addition system reachability problem: a short self-contained proof.
POPL
Jérôme Leroux
2010 — conf
Interpolating Quantifier-Free Presburger Arithmetic.
LPAR (Yogyakarta)
Daniel Kroening, Jérôme Leroux, Philipp Rümmer
2010 — conf
Place-Boundedness for Vector Addition Systems with one zero-test.
FSTTCS
Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun
2010 B conf
Reachability Analysis of Communicating Pushdown Systems.
FoSSaCS
Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre
2010 J jnl
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
Log. Methods Comput. Sci.
Jérôme Leroux
2009 A conf
A Generalization of Semenov's Theorem to Automata over Real Numbers.
CADE
Bernard Boigelot, Julien Brusten, Jérôme Leroux
2009 — conf
Polynomial Precise Interval Analysis Revisited.
Efficient Algorithms
Thomas Gawlitza, Jérôme Leroux, Jan Reineke, Helmut Seidl, Grégoire Sutre, Reinhard Wilhelm
2009 A conf
TaPAS: The Talence Presburger Arithmetic Suite.
TACAS
Jérôme Leroux, Gérald Point
2009 A* conf
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants.
LICS
Jérôme Leroux
2008 J jnl
Accelerated Data-Flow Analysis
CoRR
Jérôme Leroux, Grégoire Sutre
2008 A conf
Accelerating Interpolation-Based Model-Checking.
TACAS
Nicolas Caniart, Emmanuel Fleury, Jérôme Leroux, Marc Zeitoun
2008 J jnl
Convex Hull of Arithmetic Automata
CoRR
Jérôme Leroux
2008 B conf
Convex Hull of Arithmetic Automata.
SAS
Jérôme Leroux
2008 J jnl
Decomposition of Decidable First-Order Logics over Integers and Reals
CoRR
Florent Bouchy, Alain Finkel, Jérôme Leroux
2008 C conf
Decomposition of Decidable First-Order Logics over Integers and Reals.
TIME
Florent Bouchy, Alain Finkel, Jérôme Leroux
2008 J jnl
FAST: acceleration from theory to practice.
Int. J. Softw. Tools Technol. Transf.
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci
2008 J jnl
Structural Presburger digit vector automata.
Theor. Comput. Sci.
Jérôme Leroux
2008 J jnl
The convex hull of a regular set of integer vectors is polyhedral and effectively computable
CoRR
Alain Finkel, Jérôme Leroux
2007 B conf
Accelerated Data-Flow Analysis.
SAS
Jérôme Leroux, Grégoire Sutre
2007 — conf
Acceleration in Convex Data-Flow Analysis.
FSTTCS
Jérôme Leroux, Grégoire Sutre
2006 A* conf
FAST Extended Release.
CAV
Sébastien Bardin, Jérôme Leroux, Gérald Point
2006 — conf
Flat counter automata almost everywhere!.
Software Verification: Infinite-State Model Checking and Static Program Analysis
Jérôme Leroux, Grégoire Sutre
2006 J jnl
Least Significant Digit First Presburger Automata
CoRR
Jérôme Leroux
2005 A* conf
A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams.
LICS
Jérôme Leroux
2005 B conf
Flat Acceleration in Symbolic Model Checking.
ATVA
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Philippe Schnoebelen
2005 B conf
Flat Counter Automata Almost Everywhere!
ATVA
Jérôme Leroux, Grégoire Sutre
2005 J jnl
The convex hull of a regular set of integer vectors is polyhedral and effectively computable.
Inf. Process. Lett.
Alain Finkel, Jérôme Leroux
2004 B conf
Disjunctive Invariants for Numerical Systems.
ATVA
Jérôme Leroux
2004 A conf
FASTer Acceleration of Counter Automata in Practice.
TACAS
Sébastien Bardin, Alain Finkel, Jérôme Leroux
2004 A* conf
Image Computation in Infinite State Model Checking.
CAV
Alain Finkel, Jérôme Leroux
2004 B conf
On Flatness for 2-Dimensional Vector Addition Systems with States.
CONCUR
Jérôme Leroux, Grégoire Sutre
2004 — conf
Polynomial Time Image Computation with Interval-Definable Counters Systems.
SPIN
Alain Finkel, Jérôme Leroux
2003 A* conf
FAST: Fast Acceleration of Symbolikc Transition Systems.
CAV
Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci
2003 — conf
The Affine Hull of a Binary Automaton is Computable in Polynomial Time.
INFINITY
Jérôme Leroux
2002 — conf
How to Compose Presburger-Accelerations: Applications to Broadcast Protocols.
FSTTCS
Alain Finkel, Jérôme Leroux