# 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)**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.

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