Effective Recognizability and Model Checking of Reactive Fiffo Automata. - Grégoire Sutre; Alain Finkel; Olivier F. Roux; Franck Cassez (AMAST, 1998)

Well-Abstracted Transition Systems. - Alain Finkel; S. Purushothaman Iyer; Grégoire Sutre (CONCUR, 2000)

An Algorithm Constructing the Semilinear Post* for 2-Dim Reset/Transfer VASS. - Alain Finkel; Grégoire Sutre (MFCS, 2000)

Decidability of Reachability Problems for Classes of Two Counters Automata. - Alain Finkel; Grégoire Sutre (STACS, 2000)

Temporal-Safety Proofs for Systems Code. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; George C. Necula; Grégoire Sutre; Westley Weimer (CAV, 2002)

Verification of Embedded Reactive Fiffo Systems. - Frédéric Herbreteau; Franck Cassez; Alain Finkel; Olivier F. Roux; Grégoire Sutre (LATIN, 2002)

Lazy abstraction. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (POPL, 2002)

An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems. - Jean-Michel Couvreur; Nasser Saheb; Grégoire Sutre (LPAR, 2003)

Software Verification with BLAST. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (SPIN, 2003)

Well-abstracted transition systems: application to FIFO automata. - Alain Finkel; S. Purushothaman Iyer; Grégoire Sutre (Inf. Comput., 2003)

Modeling and verifying behavioral aspects. - François Breant; Jean-Michel Couvreur; Frédéric Gilliers; Fabrice Kordon; Isabelle Mounier; Emmanuel Paviot-Adet; Denis Poitrenaud; Dan Marius Regep; Grégoire Sutre (Formal Methods for Embedded Distributed Systems, 2004)

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

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

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)

Unfolding Concurrent Well-Structured Transition Systems. - Frédéric Herbreteau; Grégoire Sutre; The Quang Tran (TACAS, 2007)

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

Qualitative Transition Systems for the Abstraction and Comparison of Transient Behavior in Parametrized Dynamic Models. - Hayssam Soueidan; Grégoire Sutre; Macha Nikolski (CMSB, 2009)

Extrapolation-Based Path Invariants for Abstraction Refinement of Fifo Systems. - Alexander Heußner; Tristan Le Gall; Grégoire Sutre (SPIN, 2009)

Safety Verification of Communicating One-Counter Machines. - Alexander Heußner; Tristan Le Gall; Grégoire Sutre (FSTTCS, 2012)

McScM: A General Framework for the Verification of Communicating Machines. - Alexander Heußner; Tristan Le Gall; Grégoire Sutre (TACAS, 2012)

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

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

Reachability of Communicating Timed Processes. - Lorenzo Clemente; Frédéric Herbreteau; Amélie Stainer; Grégoire Sutre (FoSSaCS, 2013)

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

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

Decidable Topologies for Communicating Automata with FIFO and Bag Channels. - Lorenzo Clemente; Frédéric Herbreteau; Grégoire Sutre (CONCUR, 2014)

Hyper-Ackermannian bounds for pushdown vector addition systems. - Jérôme Leroux; M. Praveen; Grégoire Sutre (CSL-LICS, 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)

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

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)

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

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

On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems. - Vincent Penelle; Sylvain Salvati; Grégoire Sutre (FSTTCS, 2018)

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

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 Two-Dimensional Vector Addition Systems with States: One Test Is for Free. - Jérôme Leroux; Grégoire Sutre (CONCUR, 2020)

Guiding Symbolic Execution with A-Star. - Theo De Castro Pinto; Antoine Rollet; Grégoire Sutre; Ireneusz Tobor (SEFM, 2023)

An Automata-Based Approach for Synchronizable Mailbox Communication. - Romain Delpy; Anca Muscholl; Grégoire Sutre (CONCUR, 2024)

On the Send-Synchronizability Problem for Mailbox Communication. - Romain Delpy; Anca Muscholl; Grégoire Sutre (CONCUR, 2025)

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