UP | HOME

Citing Spot

Table of Contents

Generic reference

If you need to cite the Spot project, the latest tool paper about it is the following reference:

  • 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, and Henrich Lauko/. In Proc. of CAV'22, LNCS 13372, pp. 174–187. Haifa, Israel, Aug. 2022. (bib | pdf)

Tools evolve while published papers don't. Please always specify the version of Spot (or any other tool) you are using when citing it in a paper. Future versions might have different behaviors.

Other, more specific, references

Alternatively, you may also like to reference these papers to be more specific about a particular aspect of Spot.

  • Manipulating LTL formulas using Spot 1.0, Alexandre Duret-Lutz. In Proc. of ATVA'13, LNCS 8172, pp. 442–445. Hanoi, Vietnam, Oct. 2013. (bib | pdf | slides)

    This focuses on the tools ltlfilt, randltl, and ltlcross.

  • LTL translation improvements in Spot 1.0, Alexandre Duret-Lutz. Int. J. on Critical Computer-Based Systems, 5(1/2), pp. 31–54, March 2014. (bib | pdf)

    This describes the translation from LTL to TGBA used by the ltl2tgba tool.

  • Model checking using generalized testing automata, Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon. In Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI), LNCS 7400, p. 94–112, 2012. (bib | pdf)

    This describes the generalized testing automata produced by the ltl2tgta tool.

  • SAT-based minimization of deterministic ω-automata, Souheib Baarir and Alexandre Duret-Lutz. In Proc. of LPAR'15, LNCS 9450, pp. 79–87. Nov. 2015. (bib | pdf)

    This describes our SAT-based minimization technique, working with deterministic automata of arbitrary acceptance condition.

  • Practical stutter-invariance checks for ω-regular languages, Thibaud Michaud and Alexandre Duret-Lutz. In Proc. of SPIN'15, LNCS 9232, pp. 84–101. Aug. 2015. (bib | pdf)

    Explains how the stutter-invariance checks of Spot are implemented.

  • The Hanoi Omega-Automata format, Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. In Proc. of CAV'15, LNCS 9206, pp. 479–486. July 2015. (bib | pdf | slides | poster)

    Presents the automaton format supported by Spot and several other tools.

  • Generic Emptiness Check for Fun and Profit, Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejček. In. Proc. of ATVA'19, LNCS 11781, pp. 445–461, Oct 2019. (bib | pdf | slides1 | slides2)

    Presents the generic emptiness-check implemented in Spot.

  • Practical Applications of the Alternating Cycle Decomposition, Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, and Salomon Sickert. In. Proc. of TACAS'22, LNCS 13244, pp. 99–117, Apr 2022. (bib | pdf | slides1 | slides2)

    Shows applications of the ACD implemented in Spot.

  • Dissecting ltlsynt, Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, and Adrien Pommellet. In Formal Methods in System Design, 2023. (bib | pdf)

    Discuss the implementation of ltlsynt.

  • Simplifying LTL Model Checking Given Prior Knowledge, Alexandre Duret-Lutz, Denis Poitrenaud, and Yann Thierry-Mieg. In Proc. of PetriNet'25, LNCS 15714, pp. 433–456, June 2025. (bib | pdf)

    Discuss the use of implementation of autfilt --given-formula.

  • Engineering an LTLf Synthesis Tool Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman, Giuseppe De Giacomo, and Moshe Y. Vardi. In Proc. of CIAA'25. Sep. 2025. To appear. (bib)

    Discusses some of the implementation behind ltlf2dfa and ltlfsynt.

Obsolete references

  • Spot 2.0 — a framework for LTL and ω-automata manipulation, Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. In Proc. of ATVA'16, LNCS 9938, pp. 122–129. Chiba, Japan, Oct. 2016. (bib | pdf)

    This provides a quick overview of the entire project (the features of the library, the tools, the Python bindings), and provides many references detailing more specific aspects.

  • Spot: an extensible model checking library using transition-based generalized Büchi automata, Alexandre Duret-Lutz and Denis Poitrenaud. In Proc. of MASCOTS'04, pp. 76–83. Volendam, The Netherlands, Oct. 2004. Volendam. (bib | pdf)

    For a while, this used to be the only paper presenting Spot as a model-checking library.

  • Reactive Synthesis from LTL Specification with Spot, Thibaud Michaud, Maximilien Colange. In Proc. of SYNT@CAV'18. (bib | pdf)

    Was the first presentation of the tool ltlsynt. The paper Dissecting ltlsynt, mentioned earlier, is more up-to-date.