Commit 5f3cc522 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

org: add a citing page

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.
parent b2a306c8
......@@ -74,6 +74,7 @@ ORG_FILES = \
$(srcdir)/org/arch.png \
org/autfilt.org \
org/csv.org \
org/citing.org \
org/compile.org \
org/concepts.org \
org/dstar2tgba.org \
......
# -*- 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.
......@@ -57,7 +57,8 @@ The latest version is *{{{LASTRELEASE}}}* and was released on
Spot is distributed under a [[http://www.gnu.org/licenses/gpl-3.0.html][GNU GPL v3 license]].
A consequence is that if you distribute a tool built using Spot, you
*must* make the source code of that tool available as well.
*must* make the source code of that tool available as well, under a
compatible license.
* Staying in touch
......@@ -68,3 +69,8 @@ informed about future releases of Spot, we invite you to [[https://lists.lrde.ep
[[mailto:spot@lrde.epita.fr][=spot@lrde.epita.fr=]] is a list for general discussions and questions
about Spot. [[https://lists.lrde.epita.fr/listinfo/spot][Subscribe here]] if you want to join, but feel free to send
in any question (in English) or bug report without subscribing.
* Citing
Our [[file:citing.org][citing page]] has a list of papers you could cite if you need to
reference Spot in an academic publication.
......@@ -82,32 +82,12 @@ convenience, you can browse their HTML versions:
* Citing
If you want to refer to these tools in an article, please cite one of
the following articles:
If some of these tools have played a significant role in a work that
lead to some academic publication, please consider citing Spot. Our
[[file:citing.org][citing page]] has a list of papers you could cite.
- *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 =ltlfilt=, =randltl=, and =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 =ltl2tgba=
and =ltl2tgta=.
- *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 =ltl2tgta=.
Check the man page for each tool for additional references about the
algorithms or data sources used.
Additionally, the man pages of these tools also contains additional
references about the algorithms or data sources used.
# LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl
# LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment