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.

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

    Presents the tool ltlsynt.

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

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.