Citing Spot

Table of Contents

Generic reference

If you need to cite the Spot project in some academic paper, please use the following reference:

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

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. 11781, Oct 2019. (bib | pdf | slides1 | slides2)

    Presents the generic emptiness-check implemented in Spot.

Obsolete reference

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