Citing Spot

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)

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.

• 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.