| 2022 | FORTE | LTL Under Reductions with Weaker Conditions Than Stutter Invariance. | Emmanuel Paviot-Adet, Denis Poitrenaud, Etienne Renault, Yann Thierry-Mieg |
| 2019 | ICFEM | Combining Parallel Emptiness Checks with Partial Order Reductions. | Denis Poitrenaud, Etienne Renault |
| 2016 | ATVA | Heuristics for Checking Liveness Properties with Partial Order Reductions. | Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, Etienne Renault |
| 2015 | TACAS | Parallel Explicit Model Checking for Generalized Bchi Automata. | Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2013 | LPAR | Three SCC-Based Emptiness Checks for Generalized Bchi Automata. | Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2013 | TACAS | Strength-Based Decomposition of the Property Bchi Automaton for Faster Model Checking. | Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2011 | ATVA | 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 |
| 2009 | ATVA | On-the-fly Emptiness Check of Transition-Based Streett Automata. | Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur |
| 2009 | TACAS | Hierarchical Set Decision Diagrams and Regular Models. | Yann Thierry-Mieg, Denis Poitrenaud, Alexandre Hamez, Fabrice Kordon |
| 2004 | FORTE | A Symbolic Symbolic State Space Representation. | Yann Thierry-Mieg, Jean-Michel Ili, Denis Poitrenaud |
| 2004 | MASCOTS | SPOT: An Extensible Model Checking Library Using Transition-Based Generalized Bchi Automata. | Alexandre Duret-Lutz, Denis Poitrenaud |
| 2001 | TIME | Checking Linear Temporal Formulas on Sequential Recursive Petri Nets. | Serge Haddad, Denis Poitrenaud |
| 1996 | FORTE | Model Checking Based on Occurrence Net Graph. | Jean-Michel Couvreur, Denis Poitrenaud |