| 2026 | CONCUR | On Parameterized Verification over Tree Topologies. | Romain Delpy, Anca Muscholl, Grgoire Sutre |
| 2026 | FOSSACS | Bridging the Gap Between Plain VASS and Branching VASS. | Clotilde Bizire, Jrme Leroux, Grgoire Sutre |
| 2026 | MFCS | A Forward-Only Construction of Semilinear Inductive Invariants for VAS. | Clotilde Bizire, Jrme Leroux, Grgoire Sutre |
| 2025 | CONCUR | On the Send-Synchronizability Problem for Mailbox Communication. | Romain Delpy, Anca Muscholl, Grgoire Sutre |
| 2025 | MFCS | On the Reachability Problem for Two-Dimensional Branching VASS. | Clotilde Bizire, Thibault Hilaire, Jrme Leroux, Grgoire Sutre |
| 2024 | CONCUR | An Automata-Based Approach for Synchronizable Mailbox Communication. | Romain Delpy, Anca Muscholl, Grgoire Sutre |
| 2023 | SEFM | Guiding Symbolic Execution with A-Star. | Theo De Castro Pinto, Antoine Rollet, Grgoire Sutre, Ireneusz Tobor |
| 2020 | CONCUR | Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. | Jrme Leroux, Grgoire Sutre |
| 2017 | ICALP | Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. | Diego Figueira, Ranko Lazic, Jrme Leroux, Filip Mazowiecki, Grgoire Sutre |
| 2015 | ICALP | On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. | Jrme Leroux, Grgoire Sutre, Patrick Totzke |
| 2014 | ATVA | The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems. | Jrme Leroux, Vincent Penelle, Grgoire Sutre |
| 2014 | CONCUR | Decidable Topologies for Communicating Automata with FIFO and Bag Channels. | Lorenzo Clemente, Frdric Herbreteau, Grgoire Sutre |
| 2014 | CSL | Hyper-Ackermannian bounds for pushdown vector addition systems. | Jrme Leroux, M. Praveen, Grgoire Sutre |
| 2013 | CONCUR | A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness. | Jrme Leroux, M. Praveen, Grgoire Sutre |
| 2013 | FOSSACS | Reachability of Communicating Timed Processes. | Lorenzo Clemente, Frdric Herbreteau, Amlie Stainer, Grgoire Sutre |
| 2013 | LICS | On the Context-Freeness Problem for Vector Addition Systems. | Jrme Leroux, Vincent Penelle, Grgoire Sutre |
| 2012 | TACAS | McScM: A General Framework for the Verification of Communicating Machines. | Alexander Heuner, Tristan Le Gall, Grgoire Sutre |
| 2010 | FOSSACS | Reachability Analysis of Communicating Pushdown Systems. | Alexander Heuner, Jrme Leroux, Anca Muscholl, Grgoire Sutre |
| 2007 | SAS | Accelerated Data-Flow Analysis. | Jrme Leroux, Grgoire Sutre |
| 2007 | TACAS | Unfolding Concurrent Well-Structured Transition Systems. | Frdric Herbreteau, Grgoire Sutre, The Quang Tran |
| 2005 | ATVA | Flat Counter Automata Almost Everywhere! | Jrme Leroux, Grgoire Sutre |
| 2004 | CONCUR | On Flatness for 2-Dimensional Vector Addition Systems with States. | Jrme Leroux, Grgoire Sutre |
| 2003 | LPAR | An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems. | Jean-Michel Couvreur, Nasser Saheb, Grgoire Sutre |
| 2002 | CAV | Temporal-Safety Proofs for Systems Code. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grgoire Sutre, Westley Weimer |
| 2002 | LATIN | Verification of Embedded Reactive Fiffo Systems. | Frdric Herbreteau, Franck Cassez, Alain Finkel, Olivier F. Roux, Grgoire Sutre |
| 2002 | POPL | Lazy abstraction. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grgoire Sutre |
| 2000 | CONCUR | Well-Abstracted Transition Systems. | Alain Finkel, S. Purushothaman Iyer, Grgoire Sutre |
| 2000 | MFCS | An Algorithm Constructing the Semilinear Post | Alain Finkel, Grgoire Sutre |
| 2000 | STACS | Decidability of Reachability Problems for Classes of Two Counters Automata. | Alain Finkel, Grgoire Sutre |