An Efficient Algorithm for the Computation of Stubborn Sets of Well Formed Petri Nets. - Robert Brgan; Denis Poitrenaud (Application and Theory of Petri Nets, 1995)

Model Checking Based on Occurrence Net Graph. - Jean-Michel Couvreur; Denis Poitrenaud (FORTE, 1996)

Detection of Illegal Behaviors Based on Unfoldings. - Jean-Michel Couvreur; Denis Poitrenaud (ICATPN, 1999)

Theoretical Aspects of Recursive Petri Nets. - Serge Haddad; Denis Poitrenaud (ICATPN, 1999)

Multimedia Information Systems: Towards a Design Methodology Based on Spatio-Temporal Relations, Petri Nets, and ECA Rules. - Sabine Boufenara; Zizette Boufriche-Boufaïda; Mahmoud Boufaïda; Denis Poitrenaud (ADVIS, 2000)

Designing a LTL Model-Checker Based on Unfolding Graphs. - Jean-Michel Couvreur; Sébastien Grivet; Denis Poitrenaud (ICATPN, 2000)

Pre- and Post-agglomerations for LTL Model Checking. - Denis Poitrenaud; Jean-François Pradat-Peyre (ICATPN, 2000)

Unfolding of Products of Symmetrical Petri Nets. - Jean-Michel Couvreur; Sébastien Grivet; Denis Poitrenaud (ICATPN, 2001)

Checking Linear Temporal Formulas on Sequential Recursive Petri Nets. - Serge Haddad; Denis Poitrenaud (TIME, 2001)

The Barrier-Lock Clock: A Scalable Synchronization-Oriented Logical Clock. - Luciana Bezerra Arantes; Denis Poitrenaud; Pierre Sens 001; Bertil Folliot (Parallel Process. Lett., 2001)

Data Decision Diagrams for Petri Net Analysis. - Jean-Michel Couvreur; Emmanuelle Encrenaz; Emmanuel Paviot-Adet; Denis Poitrenaud; Pierre-André Wacrenier (ICATPN, 2002)

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)

A Symbolic Symbolic State Space Representation. - Yann Thierry-Mieg; Jean-Michel Ilié; Denis Poitrenaud (FORTE, 2004)

SPOT: An Extensible Model Checking Library Using Transition-Based Generalized Büchi Automata. - Alexandre Duret-Lutz; Denis Poitrenaud (MASCOTS, 2004)

On-the-Fly Emptiness Checks for Generalized Büchi Automata. - Jean-Michel Couvreur; Alexandre Duret-Lutz; Denis Poitrenaud (SPIN, 2005)

Recursive Petri nets. - Serge Haddad; Denis Poitrenaud (Acta Informatica, 2007)

MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. - Kais Klai; Denis Poitrenaud (Petri Nets, 2008)

On-the-fly Emptiness Check of Transition-Based Streett Automata. - Alexandre Duret-Lutz; Denis Poitrenaud; Jean-Michel Couvreur (ATVA, 2009)

Complementary Formal Approaches for Dependability Analysis. - Souheib Baarir; Cécile Braunstein; Renaud Clavel; Emmanuelle Encrenaz; Jean-Michel Ilié; Régis Leveugle; Isabelle Mounier; Laurence Pierre; Denis Poitrenaud (DFT, 2009)

Hierarchical Set Decision Diagrams and Regular Models. - Yann Thierry-Mieg; Denis Poitrenaud; Alexandre Hamez; Fabrice Kordon (TACAS, 2009)

Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking. - Alexandre Duret-Lutz; Kais Klai; Denis Poitrenaud; Yann Thierry-Mieg (ATVA, 2011)

Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking - Alexandre Duret-Lutz; Kais Klai; Denis Poitrenaud; Yann Thierry-Mieg (CoRR, 2011)

Feasibility analysis for robustness quantification by symbolic model checking. - Souheib Baarir; Cécile Braunstein; Emmanuelle Encrenaz; Jean-Michel Ilié; Isabelle Mounier; Denis Poitrenaud; Sana Younès (Formal Methods Syst. Des., 2011)

Three SCC-Based Emptiness Checks for Generalized Büchi Automata. - Etienne Renault; Alexandre Duret-Lutz; Fabrice Kordon; Denis Poitrenaud (LPAR, 2013)

Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking. - Etienne Renault; Alexandre Duret-Lutz; Fabrice Kordon; Denis Poitrenaud (TACAS, 2013)

Branching Processes of General Petri Nets. - Jean-Michel Couvreur; Denis Poitrenaud; Pascal Weil (Fundam. Informaticae, 2013)

Parallel Explicit Model Checking for Generalized Büchi Automata. - Etienne Renault; Alexandre Duret-Lutz; Fabrice Kordon; Denis Poitrenaud (TACAS, 2015)

Heuristics for Checking Liveness Properties with Partial Order Reductions. - Alexandre Duret-Lutz; Fabrice Kordon; Denis Poitrenaud; Etienne Renault (ATVA, 2016)

Variations on parallel explicit emptiness checks for generalized Büchi automata. - Etienne Renault; Alexandre Duret-Lutz; Fabrice Kordon; Denis Poitrenaud (Int. J. Softw. Tools Technol. Transf., 2017)

Combining Parallel Emptiness Checks with Partial Order Reductions. - Denis Poitrenaud; Etienne Renault (ICFEM, 2019)

LTL Under Reductions with Weaker Conditions Than Stutter Invariance. - Emmanuel Paviot-Adet; Denis Poitrenaud; Etienne Renault; Yann Thierry-Mieg (FORTE, 2022)

A model-checker exploiting structural reductions even with stutter sensitive LTL. - Yann Thierry-Mieg; Etienne Renault; Emmanuel Paviot-Adet; Denis Poitrenaud (Sci. Comput. Program., 2024)

Simplifying LTL Model Checking Given Prior Knowledge. - Alexandre Duret-Lutz; Denis Poitrenaud; Yann Thierry-Mieg (Petri Nets, 2025)

Structural Reductions and Stutter Sensitive Properties. - Emmanuel Paviot-Adet; Denis Poitrenaud; Etienne Renault; Yann Thierry-Mieg (Log. Methods Comput. Sci., 2025)