How to Compose Presburger-Accelerations: Applications to Broadcast Protocols. - Alain Finkel; Jérôme Leroux (FSTTCS, 2002)

FAST: Fast Acceleration of Symbolikc Transition Systems. - Sébastien Bardin; Alain Finkel; Jérôme Leroux; Laure Petrucci (CAV, 2003)

The Affine Hull of a Binary Automaton is Computable in Polynomial Time. - Jérôme Leroux (INFINITY, 2003)

Disjunctive Invariants for Numerical Systems. - Jérôme Leroux (ATVA, 2004)

Image Computation in Infinite State Model Checking. - Alain Finkel; Jérôme Leroux (CAV, 2004)

On Flatness for 2-Dimensional Vector Addition Systems with States. - Jérôme Leroux; Grégoire Sutre (CONCUR, 2004)

Polynomial Time Image Computation with Interval-Definable Counters Systems. - Alain Finkel; Jérôme Leroux (SPIN, 2004)

FASTer Acceleration of Counter Automata in Practice. - Sébastien Bardin; Alain Finkel; Jérôme Leroux (TACAS, 2004)

Flat Acceleration in Symbolic Model Checking. - Sébastien Bardin; Alain Finkel; Jérôme Leroux; Philippe Schnoebelen (ATVA, 2005)

Flat Counter Automata Almost Everywhere! - Jérôme Leroux; Grégoire Sutre (ATVA, 2005)

A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams. - Jérôme Leroux (LICS, 2005)

The convex hull of a regular set of integer vectors is polyhedral and effectively computable. - Alain Finkel; Jérôme Leroux (Inf. Process. Lett., 2005)

FAST Extended Release. - Sébastien Bardin; Jérôme Leroux; Gérald Point (CAV, 2006)

Least Significant Digit First Presburger Automata - Jérôme Leroux (CoRR, 2006)

Acceleration in Convex Data-Flow Analysis. - Jérôme Leroux; Grégoire Sutre (FSTTCS, 2007)

Accelerated Data-Flow Analysis. - Jérôme Leroux; Grégoire Sutre (SAS, 2007)

Convex Hull of Arithmetic Automata. - Jérôme Leroux (SAS, 2008)

Accelerating Interpolation-Based Model-Checking. - Nicolas Caniart; Emmanuel Fleury; Jérôme Leroux; Marc Zeitoun (TACAS, 2008)

Decomposition of Decidable First-Order Logics over Integers and Reals. - Florent Bouchy; Alain Finkel; Jérôme Leroux (TIME, 2008)

FAST: acceleration from theory to practice. - Sébastien Bardin; Alain Finkel; Jérôme Leroux; Laure Petrucci (Int. J. Softw. Tools Technol. Transf., 2008)

Structural Presburger digit vector automata. - Jérôme Leroux (Theor. Comput. Sci., 2008)

Polynomial Precise Interval Analysis Revisited. - Thomas Gawlitza; Jérôme Leroux; Jan Reineke 001; Helmut Seidl; Grégoire Sutre; Reinhard Wilhelm (Efficient Algorithms, 2009)

A Generalization of Semenov's Theorem to Automata over Real Numbers. - Bernard Boigelot; Julien Brusten; Jérôme Leroux (CADE, 2009)

TaPAS: The Talence Presburger Arithmetic Suite. - Jérôme Leroux; Gérald Point (TACAS, 2009)

Place-Boundedness for Vector Addition Systems with one zero-test. - Rémi Bonnet; Alain Finkel; Jérôme Leroux; Marc Zeitoun (FSTTCS, 2010)

Interpolating Quantifier-Free Presburger Arithmetic. - Daniel Kroening; Jérôme Leroux; Philipp Rümmer (LPAR (Yogyakarta), 2010)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants - Jérôme Leroux (Log. Methods Comput. Sci., 2010)

The BINCOA Framework for Binary Code Analysis. - Sébastien Bardin; Philippe Herrmann; Jérôme Leroux; Olivier Ly; Renaud Tabary; Aymeric Vincent (CAV, 2011)

Vector Addition System Reachability Problem: A Short Self-contained Proof. - Jérôme Leroux (LATA, 2011)

Vector Addition Systems Reachability Problem (A Simpler Solution). - Jérôme Leroux (Turing-100, 2012)

Model Checking Vector Addition Systems with one zero-test - Rémi Bonnet; Alain Finkel; Jérôme Leroux; Marc Zeitoun (Log. Methods Comput. Sci., 2012)

Reachability Analysis of Communicating Pushdown Systems - Alexander Heußner; Jérôme Leroux; Anca Muscholl; Grégoire Sutre (Log. Methods Comput. Sci., 2012)

Acceleration for Petri Nets. - Jérôme Leroux (ATVA, 2013)

Acceleration For Presburger Petri Nets. - Jérôme Leroux (VPT@CAV, 2013)

A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness. - Jérôme Leroux; M. Praveen; Grégoire Sutre (CONCUR, 2013)

Presburger Vector Addition Systems. - Jérôme Leroux (LICS, 2013)

On the Context-Freeness Problem for Vector Addition Systems. - Jérôme Leroux; Vincent Penelle; Grégoire Sutre (LICS, 2013)

Vector Addition System Reversible Reachability Problem - Jérôme Leroux (Log. Methods Comput. Sci., 2013)

The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems. - Jérôme Leroux; Vincent Penelle; Grégoire Sutre (ATVA, 2014)

Hyper-Ackermannian bounds for pushdown vector addition systems. - Jérôme Leroux; M. Praveen; Grégoire Sutre (CSL-LICS, 2014)

On Functions Weakly Computable by Petri Nets and Vector Addition Systems. - Jérôme Leroux; Philippe Schnoebelen (RP, 2014)

Neue, einfache Algorithmen für Petrinetze. - Alain Finkel; Jérôme Leroux (Inform. Spektrum, 2014)

On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. - Jérôme Leroux; Grégoire Sutre; Patrick Totzke (ICALP (2), 2015)

Demystifying Reachability in Vector Addition Systems. - Jérôme Leroux; Sylvain Schmitz (LICS, 2015)

On Boundedness Problems for Pushdown Vector Addition Systems. - Jérôme Leroux; Grégoire Sutre; Patrick Totzke (RP, 2015)

Structurally Cyclic Petri Nets. - Frank Drewes; Jérôme Leroux (Log. Methods Comput. Sci., 2015)

Reachability in Vector Addition Systems Demystified. - Jérôme Leroux; Sylvain Schmitz (CoRR, 2015)

Recent and simple algorithms for Petri nets. - Alain Finkel; Jérôme Leroux (Softw. Syst. Model., 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)

Model Checking Population Protocols. - Javier Esparza; Pierre Ganty; Jérôme Leroux; Rupak Majumdar (FSTTCS, 2016)

Ideal Decompositions for Vector Addition Systems (Invited Talk). - Jérôme Leroux; Sylvain Schmitz (STACS, 2016)

Guiding Craig interpolation with domain-specific abstractions. - Jérôme Leroux; Philipp Rümmer; Pavle Subotic (Acta Informatica, 2016)

Preface. - Parosh Aziz Abdulla; Stéphane Demri; Alain Finkel; Jérôme Leroux; Igor Potapov (Fundam. Informaticae, 2016)

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)

Linear combinations of unordered data vectors. - Piotr Hofman; Jérôme Leroux; Patrick Totzke (LICS, 2017)

Backward coverability with pruning for lossy channel systems. - Thomas Geffroy; Jérôme Leroux; Grégoire Sutre (SPIN, 2017)

Verification of population protocols. - Javier Esparza; Pierre Ganty; Jérôme Leroux; Rupak Majumdar (Acta Informatica, 2017)

Reachability for Two-Counter Machines with One Test and One Reset. - Alain Finkel; Jérôme Leroux; Grégoire Sutre (FSTTCS, 2018)

Polynomial Vector Addition Systems With States. - Jérôme Leroux (ICALP, 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)

Occam's Razor applied to the Petri net coverability problem. - Thomas Geffroy; Jérôme Leroux; Grégoire Sutre (Theor. Comput. Sci., 2018)

Distance Between Mutually Reachable Petri Net Configurations. - Jérôme Leroux (FSTTCS, 2019)

Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. - Jérôme Leroux; Sylvain Schmitz (LICS, 2019)

Petri Net Reachability Problem (Invited Talk). - Jérôme Leroux (MFCS, 2019)

Co-Finiteness and Co-Emptiness of Reachability Sets in Vector Addition Systems with States. - Petr Jancar; Jérôme Leroux; Grégoire Sutre (Fundam. Informaticae, 2019)

On Functions Weakly Computable by Pushdown Petri Nets and Related Systems. - Jérôme Leroux; M. Praveen; Philippe Schnoebelen; Grégoire Sutre (Log. Methods Comput. Sci., 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)

Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. - Jérôme Leroux; Grégoire Sutre (CONCUR, 2020)

Efficient Analysis of VASS Termination Complexity. - Antonín Kucera 001; Jérôme Leroux; Dominik Velan (LICS, 2020)

When Reachability Meets Grzegorczyk. - Jérôme Leroux (LICS, 2020)

Flat Petri Nets (Invited Talk). - Jérôme Leroux (Petri Nets, 2021)

The Reachability Problem for Petri Nets is Not Primitive Recursive. - Jérôme Leroux (FOCS, 2021)

New Algorithms for Combinations of Objectives using Separating Automata. - Ashwani Anand; Nathanaël Fijalkow; Aliénor Goubault-Larrecq; Jérôme Leroux; Pierre Ohlmann (GandALF, 2021)

State Complexity of Counting Population Protocols With Leaders. - Jérôme Leroux (CoRR, 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 Petri Nets Is Not Elementary. - Wojciech Czerwinski; Slawomir Lasota 001; Ranko Lazic 001; Jérôme Leroux; Filip Mazowiecki (J. ACM, 2021)

State Complexity of Protocols with Leaders. - Jérôme Leroux (PODC, 2022)

Semilinear Home-space is Decidable for Petri Nets. - Petr Jancar; Jérôme Leroux (CoRR, 2022)

Compiling Petri Net Mutual Reachability in Presburger. - Jérôme Leroux (CoRR, 2022)

The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. - Petr Jancar; Jérôme Leroux (CONCUR, 2023)

New Lower Bounds for Reachability in Vector Addition Systems. - Wojciech Czerwinski; Ismaël Jecker; Slawomir Lasota 001; Jérôme Leroux; Lukasz Orlikowski (FSTTCS, 2023)

Lower bounds on the state complexity of population protocols. - Philipp Czerner; Javier Esparza; Jérôme Leroux (Distributed Comput., 2023)

On the Home-Space Problem for Petri Nets. - Petr Jancar; Jérôme Leroux (Taming the Infinities of Concurrency, 2024)

Invariants for One-Counter Automata with Disequality Tests. - Dmitry Chistikov 001; Jérôme Leroux; Henry Sinclair-Banks; Nicolas Waldburger (CONCUR, 2024)

Ackermannian Completion of Separators. - Jérôme Leroux (FoSSaCS (1), 2024)

A State-of-the-Art Karp-Miller Algorithm Certified in Coq. - Thibault Hilaire; David Ilcinkas; Jérôme Leroux (TACAS (1), 2024)

On the Home-Space Problem for Petri Nets and its Ackermannian Complexity. - Petr Jancar; Jérôme Leroux (Log. Methods Comput. Sci., 2024)

Structural Liveness of Conservative Petri Nets. - Petr Jancar; Jérôme Leroux; Jiri Valusek (FoSSaCS, 2025)

On the Reachability Problem for Two-Dimensional Branching VASS. - Clotilde Bizière; Thibault Hilaire; Jérôme Leroux; Grégoire Sutre (MFCS, 2025)

Preface to special issue MFCS 2023. - Jérôme Leroux; David Peleg (Inf. Comput., 2025)