b439fc674b
With a reference to the "to appear" ATVA'16 paper. * doc/org/citing.org: New file. * doc/Makefile.am: Add it. * doc/org/index.org, doc/org/tools.org: Link to it.
79 lines
4.3 KiB
Org Mode
79 lines
4.3 KiB
Org Mode
# -*- 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:
|
||
|
||
- *Spot 2.0 –- a framework for LTL and ω-automata manipulation*,
|
||
/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.
|