Generic Programming Redesign of Patterns. - Thierry Géraud; Alexandre Duret-Lutz (EuroPLoP, 2000)

Obtaining Genericity for Image Processing and Pattern Recognition Algorithms. - Thierry Géraud; Yoann Fabre; Alexandre Duret-Lutz (ICPR, 2000)

Expression Templates in Ada. - Alexandre Duret-Lutz (Ada-Europe, 2001)

Design Patterns for Generic Programming in C++. - Alexandre Duret-Lutz; Thierry Géraud; Akim Demaille (COOTS, 2001)

Multiband segmentation using morphological clustering and fusion $application to color image segmentation. - H. Xue; Thierry Géraud; Alexandre Duret-Lutz (ICIP (1), 2003)

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)

Emptiness Check of Powerset Buchi Automata using Inclusion Tests. - Souheib Baarir; Alexandre Duret-Lutz (ACSD, 2007)

Flattening the Viewable Sphere. - Daniel M. Germán; Lloyd Burchill; Alexandre Duret-Lutz; Sébastien Pérez-Duarte; Emmanuel Pérez-Duarte; Josh Sommers (CAe, 2007)

An XML Format Proposal for the Description of Weighted Automata, Transducers and Regular Expressions. - Akim Demaille; Alexandre Duret-Lutz; Florian Lesaint; Sylvain Lombardy; Jacques Sakarovitch; Florent Terrones (FSMNLP, 2008)

On-the-fly Emptiness Check of Transition-Based Streett Automata. - Alexandre Duret-Lutz; Denis Poitrenaud; Jean-Michel Couvreur (ATVA, 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)

Model Checking Using Generalized Testing Automata. - Ala-Eddine Ben Salem; Alexandre Duret-Lutz; Fabrice Kordon (Trans. Petri Nets Other Model. Concurr., 2012)

Manipulating LTL Formulas Using Spot 1.0. - Alexandre Duret-Lutz (ATVA, 2013)

LTL Model Checking with Neco. - Lukasz Fronc; Alexandre Duret-Lutz (ATVA, 2013)

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

Compositional Approach to Suspension and Other Improvements to LTL Translation. - Tomás Babiak; Thomas Badie; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 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)

Implementation Concepts in Vaucanson 2. - Akim Demaille; Alexandre Duret-Lutz; Sylvain Lombardy; Jacques Sakarovitch (CIAA, 2013)

Mechanizing the Minimization of Deterministic Generalized Büchi Automata. - Souheib Baarir; Alexandre Duret-Lutz (FORTE, 2014)

Is there a best büchi automaton for explicit model checking? - Frantisek Blahoudek; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 2014)

Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata. - Ala-Eddine Ben Salem; Alexandre Duret-Lutz; Fabrice Kordon; Yann Thierry-Mieg (TACAS, 2014)

A Type System for Weighted Automata and Rational Expressions. - Akim Demaille; Alexandre Duret-Lutz; Sylvain Lombardy; Luca Saiu; Jacques Sakarovitch (CIAA, 2014)

LTL translation improvements in Spot 1.0. - Alexandre Duret-Lutz (Int. J. Crit. Comput. Based Syst., 2014)

The Hanoi Omega-Automata Format. - Tomás Babiak; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; Jan Kretínský; David Müller 001; David Parker 001; Jan Strejcek (CAV (1), 2015)

SAT-Based Minimization of Deterministic omega -Automata. - Souheib Baarir; Alexandre Duret-Lutz (LPAR, 2015)

On Refinement of Büchi Automata for Explicit Model Checking. - Frantisek Blahoudek; Alexandre Duret-Lutz; Vojtech Rujbr; Jan Strejcek (SPIN, 2015)

Practical Stutter-Invariance Checks for ω-Regular Languages. - Thibaud Michaud; Alexandre Duret-Lutz (SPIN, 2015)

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)

Spot 2.0 - A Framework for LTL and omega -Automata Manipulation. - Alexandre Duret-Lutz; Alexandre Lewkowicz; Amaury Fauchille; Thibaud Michaud; Etienne Renault; Laurent Xu (ATVA, 2016)

Seminator: A Tool for Semi-Determinization of Omega-Automata. - Frantisek Blahoudek; Alexandre Duret-Lutz; Mikulás Klokocka; Mojmír Kretínský; Jan Strejcek (LPAR, 2017)

Explicit state model checking with generalized Büchi and Rabin automata. - Vincent Bloemen; Alexandre Duret-Lutz; Jaco van de Pol (SPIN, 2017)

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)

Parallel Model Checking Algorithms for Linear-Time Temporal Logic. - Jiri Barnat; Vincent Bloemen; Alexandre Duret-Lutz; Alfons Laarman; Laure Petrucci; Jaco van de Pol; Etienne Renault (Handbook of Parallel Constraint Reasoning, 2018)

Generic Emptiness Check for Fun and Profit. - Christel Baier; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; David Müller 001; Jan Strejcek (ATVA, 2019)

Model checking with generalized Rabin and Fin-less automata. - Vincent Bloemen; Alexandre Duret-Lutz; Jaco van de Pol (Int. J. Softw. Tools Technol. Transf., 2019)

Practical "Paritizing" of Emerson-Lei Automata. - Florian Renkin; Alexandre Duret-Lutz; Adrien Pommellet (ATVA, 2020)

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. - Frantisek Blahoudek; Alexandre Duret-Lutz; Jan Strejcek (CAV (2), 2020)

From Spot 2.0 to Spot 2.10: What's New? - Alexandre Duret-Lutz; Etienne Renault; Maximilien Colange; Florian Renkin; Alexandre Gbaguidi Aisse; Philipp Schlehuber-Caissier; Thomas Medioni; Antoine Martin; Jérôme Dubois; Clément Gillard; Henrich Lauko (CAV (2), 2022)

Effective Reductions of Mealy Machines. - Florian Renkin; Philipp Schlehuber-Caissier; Alexandre Duret-Lutz; Adrien Pommellet (FORTE, 2022)

Practical Applications of the Alternating Cycle Decomposition. - Antonio Casares; Alexandre Duret-Lutz; Klara J. Meyer; Florian Renkin; Salomon Sickert (TACAS (2), 2022)

Improvements to ltlsynt. - Florian Renkin; Philipp Schlehuber; Alexandre Duret-Lutz; Adrien Pommellet (CoRR, 2022)

Dissecting ltlsynt. - Florian Renkin; Philipp Schlehuber-Caissier; Alexandre Duret-Lutz; Adrien Pommellet (Formal Methods Syst. Des., 2022)

The Mealy-machine reduction functions of Spot. - Florian Renkin; Philipp Schlehuber-Caissier; Alexandre Duret-Lutz; Adrien Pommellet (Sci. Comput. Program., 2023)

Translation of Semi-extended Regular Expressions Using Derivatives. - Antoine Martin; Etienne Renault; Alexandre Duret-Lutz (CIAA, 2024)

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021. - Swen Jacobs; Guillermo A. Pérez 001; Remco Abraham; Véronique Bruyère; Michaël Cadilhac; Maximilien Colange; Charly Delfosse; Tom van Dijk; Alexandre Duret-Lutz; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; et al. (Int. J. Softw. Tools Technol. Transf., 2024)

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

Engineering an LTLf Synthesis Tool. - Alexandre Duret-Lutz; Shufang Zhu 001; Nir Piterman; Giuseppe De Giacomo; Moshe Y. Vardi (CoRR, 2025)