| 2026 | FOSSACS | Bridging the Gap Between Plain VASS and Branching VASS. | Clotilde Bizire, Jrme Leroux, Grgoire Sutre |
| 2026 | LICS | Reachability in VASS Extended with Integer Counters. | Clotilde Bizire, Wojciech Czerwinski, Roland Guttenberg, Jrme Leroux, Vincent Michielini, Lukasz Orlikowski, Antoni Puch, Henry Sinclair-Banks |
| 2026 | MFCS | A Forward-Only Construction of Semilinear Inductive Invariants for VAS. | Clotilde Bizire, Jrme Leroux, Grgoire Sutre |
| 2025 | FOSSACS | Structural Liveness of Conservative Petri Nets. | Petr Jancar, Jrme Leroux, Jiri Valusek |
| 2025 | MFCS | On the Reachability Problem for Two-Dimensional Branching VASS. | Clotilde Bizire, Thibault Hilaire, Jrme Leroux, Grgoire Sutre |
| 2024 | CONCUR | Invariants for One-Counter Automata with Disequality Tests. | Dmitry Chistikov, Jrme Leroux, Henry Sinclair-Banks, Nicolas Waldburger |
| 2024 | FOSSACS | Ackermannian Completion of Separators. | Jrme Leroux |
| 2024 | TACAS | A State-of-the-Art Karp-Miller Algorithm Certified in Coq. | Thibault Hilaire, David Ilcinkas, Jrme Leroux |
| 2023 | CONCUR | The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. | Petr Jancar, Jrme Leroux |
| 2022 | PODC | State Complexity of Protocols with Leaders. | Jrme Leroux |
| 2021 | FOCS | The Reachability Problem for Petri Nets is Not Primitive Recursive. | Jrme Leroux |
| 2020 | CONCUR | Reachability in Fixed Dimension Vector Addition Systems with States. | Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Filip Mazowiecki |
| 2020 | CONCUR | Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. | Jrme Leroux, Grgoire Sutre |
| 2020 | LICS | Efficient Analysis of VASS Termination Complexity. | Antonn Kucera, Jrme Leroux, Dominik Velan |
| 2020 | LICS | When Reachability Meets Grzegorczyk. | Jrme Leroux |
| 2019 | LICS | Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. | Jrme Leroux, Sylvain Schmitz |
| 2019 | MFCS | Petri Net Reachability Problem (Invited Talk). | Jrme Leroux |
| 2019 | STOC | The reachability problem for Petri nets is not elementary. | Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Filip Mazowiecki |
| 2018 | ICALP | Polynomial Vector Addition Systems With States. | Jrme Leroux |
| 2017 | ICALP | Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. | Diego Figueira, Ranko Lazic, Jrme Leroux, Filip Mazowiecki, Grgoire Sutre |
| 2017 | LICS | Linear combinations of unordered data vectors. | Piotr Hofman, Jrme Leroux, Patrick Totzke |
| 2016 | FOSSACS | Coverability Trees for Petri Nets with Unordered Data. | Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jrme Leroux, Sylvain Schmitz, Patrick Totzke |
| 2016 | STACS | Ideal Decompositions for Vector Addition Systems (Invited Talk). | Jrme Leroux, Sylvain Schmitz |
| 2015 | CONCUR | Verification of Population Protocols. | Javier Esparza, Pierre Ganty, Jrme Leroux, Rupak Majumdar |
| 2015 | ICALP | On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. | Jrme Leroux, Grgoire Sutre, Patrick Totzke |
| 2015 | LICS | Demystifying Reachability in Vector Addition Systems. | Jrme Leroux, Sylvain Schmitz |
| 2014 | ATVA | The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems. | Jrme Leroux, Vincent Penelle, Grgoire Sutre |
| 2014 | CSL | Hyper-Ackermannian bounds for pushdown vector addition systems. | Jrme Leroux, M. Praveen, Grgoire Sutre |
| 2013 | ATVA | Acceleration for Petri Nets. | Jrme Leroux |
| 2013 | CAV | Acceleration For Presburger Petri Nets. | Jrme Leroux |
| 2013 | CONCUR | A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness. | Jrme Leroux, M. Praveen, Grgoire Sutre |
| 2013 | LICS | Presburger Vector Addition Systems. | Jrme Leroux |
| 2013 | LICS | On the Context-Freeness Problem for Vector Addition Systems. | Jrme Leroux, Vincent Penelle, Grgoire Sutre |
| 2011 | CAV | The BINCOA Framework for Binary Code Analysis. | Sbastien Bardin, Philippe Herrmann, Jrme Leroux, Olivier Ly, Renaud Tabary, Aymeric Vincent |
| 2011 | CONCUR | Vector Addition System Reversible Reachability Problem. | Jrme Leroux |
| 2011 | LATA | Vector Addition System Reachability Problem: A Short Self-contained Proof. | Jrme Leroux |
| 2011 | POPL | Vector addition system reachability problem: a short self-contained proof. | Jrme Leroux |
| 2010 | FOSSACS | Reachability Analysis of Communicating Pushdown Systems. | Alexander Heuner, Jrme Leroux, Anca Muscholl, Grgoire Sutre |
| 2010 | LPAR | Interpolating Quantifier-Free Presburger Arithmetic. | Daniel Kroening, Jrme Leroux, Philipp Rmmer |
| 2009 | CADE | A Generalization of Semenov's Theorem to Automata over Real Numbers. | Bernard Boigelot, Julien Brusten, Jrme Leroux |
| 2009 | LICS | The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. | Jrme Leroux |
| 2009 | TACAS | TaPAS: The Talence Presburger Arithmetic Suite. | Jrme Leroux, Grald Point |
| 2008 | SAS | Convex Hull of Arithmetic Automata. | Jrme Leroux |
| 2008 | TACAS | Accelerating Interpolation-Based Model-Checking. | Nicolas Caniart, Emmanuel Fleury, Jrme Leroux, Marc Zeitoun |
| 2008 | TIME | Decomposition of Decidable First-Order Logics over Integers and Reals. | Florent Bouchy, Alain Finkel, Jrme Leroux |
| 2007 | SAS | Accelerated Data-Flow Analysis. | Jrme Leroux, Grgoire Sutre |
| 2006 | CAV | FAST Extended Release. | Sbastien Bardin, Jrme Leroux, Grald Point |
| 2005 | ATVA | Flat Acceleration in Symbolic Model Checking. | Sbastien Bardin, Alain Finkel, Jrme Leroux, Philippe Schnoebelen |
| 2005 | ATVA | Flat Counter Automata Almost Everywhere! | Jrme Leroux, Grgoire Sutre |
| 2005 | LICS | A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams. | Jrme Leroux |
| 2004 | ATVA | Disjunctive Invariants for Numerical Systems. | Jrme Leroux |
| 2004 | CAV | Image Computation in Infinite State Model Checking. | Alain Finkel, Jrme Leroux |
| 2004 | CONCUR | On Flatness for 2-Dimensional Vector Addition Systems with States. | Jrme Leroux, Grgoire Sutre |
| 2004 | TACAS | FASTer Acceleration of Counter Automata in Practice. | Sbastien Bardin, Alain Finkel, Jrme Leroux |
| 2003 | CAV | FAST: Fast Acceleration of Symbolikc Transition Systems. | Sbastien Bardin, Alain Finkel, Jrme Leroux, Laure Petrucci |