citing.org 5.29 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
# -*- coding: utf-8 -*-
#+TITLE: Citing Spot
#+DESCRIPTION: Paper related to Spot
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
5
6
7
8
9
10
11
#+HTML_LINK_UP: index.html

* Generic reference

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

12
- *Spot 2.0 — a framework for LTL and ω-automata manipulation*,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
  /Alexandre Duret-Lutz/, /Alexandre Lewkowicz/, /Amaury Fauchille/,
14
15
16
  /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]])
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

  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/.
35
36
  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]])
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
38
39
40
41
42
43

  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
44
  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]])
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67

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

68
  Presents the automaton format [[file:hoa.org][supported by Spot]] and [[http://adl.github.io/hoaf/support.html][several other
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
69
70
  tools]].

71
72
- *Reactive Synthesis from LTL Specification with Spot*,
  /Thibaud Michaud/, /Maximilien Colange/.
73
  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]])
74
75

  Presents the tool [[file:ltlsynt.org][=ltlsynt=]].
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76

77
78
79
80
81
82
83
84
- *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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
85
86
87
88
89
90
91
92
93
* 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.