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