citing.org 4.34 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
# -*- coding: utf-8 -*-
#+TITLE: Citing Spot
#+DESCRIPTION: Paper related to Spot
#+SETUPFILE: 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:

12
- *Spot 2.0 — a framework for LTL and ω-automata manipulation*,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
  /Alexandre Duret-Lutz/, /Alexandre Lewkowicz/, /Amaury Fauchille/,
  /Thibaud Michaud/, /Etienne Renault/, and /Laurent Xu/.  To appear
  in Proc. of ATVA'16.  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):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), 7400: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 2.0]] and [[http://adl.github.io/hoaf/support.html][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.  ([[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.