# -*- coding: utf-8 -*-
#+TITLE: Citing Spot
#+DESCRIPTION: Paper related to Spot
#+INCLUDE: setup.org
#+HTML_LINK_UP: index.html

* 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.
  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.16.atva2][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][pdf]])

  This provides a quick overview of the entire project (the features
  of the library, [[file:tools.org][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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]])

  This focuses on the tools [[file:ltlfilt.org][=ltlfilt=]], [[file:randltl.org][=randltl=]], and [[file:ltlcross.org][=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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])

  This describes the translation from LTL to TGBA used by the
  [[file:ltl2tgba.org][=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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#bensalem.12.topnoc][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/bensalem.12.topnoc.pdf][pdf]])

  This describes the generalized testing automata produced by the
  [[file:ltl2tgta.org][=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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#baarir.15.lpar][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.15.lpar.pdf][pdf]])

  This describes our [[file:satmin.org][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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#michaud.15.spin][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#babiak.15.cav][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.pdf][pdf]] |
  [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.slides.pdf][slides]] | [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.poster.pdf][poster]])

  Presents the automaton format [[file:hoa.org][supported by Spot]] and [[http://adl.github.io/hoaf/support.html][several other
  tools]].

- *Reactive Synthesis from LTL Specification with Spot*,
  /Thibaud Michaud/, /Maximilien Colange/.
  In Proc. of SYNT@CAV'18.  ([[https://www.lrde.epita.fr/~max/bibtexbrowser.php?key=michaud.18.synt&bib=perso.bib][bib]] | [[https://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf][pdf]])

  Presents the tool [[file:ltlsynt.org][=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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#baier.19.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.pdf][pdf]] |
  [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.slides.mefosyloma.pdf][slides1]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baier.19.atva.slides.pdf][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.  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.04.mascots][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.04.mascots.draft.pdf][pdf]])

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

#  LocalWords:  utf html Alexandre Duret Lutz Lewkowicz Amaury Xu pdf
#  LocalWords:  Fauchille Thibaud Michaud Etienne Proc ATVA LNCS TGBA
#  LocalWords:  ltlfilt randltl ltlcross tgba Eddine Fabrice Kordon
#  LocalWords:  Petri ToPNoC tgta Souheib Baarir LPAR Tomáš Babiak
#  LocalWords:  František Blahoudek Joachim Křetínský Müller Strejček
#  LocalWords:  CAV Maximilien Colange ltlsynt Christel Baier
#  LocalWords:  Poitrenaud Volendam