From b439fc674be3f2aae3641fe2d96eded63ff9f289 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 15:06:15 +0200 Subject: [PATCH] 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. --- doc/Makefile.am | 1 + doc/org/citing.org | 79 ++++++++++++++++++++++++++++++++++++++++++++++ doc/org/index.org | 8 ++++- doc/org/tools.org | 30 +++--------------- 4 files changed, 92 insertions(+), 26 deletions(-) create mode 100644 doc/org/citing.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 292b37da2..3cf97632f 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 \ diff --git a/doc/org/citing.org b/doc/org/citing.org new file mode 100644 index 000000000..8f9e4dc06 --- /dev/null +++ b/doc/org/citing.org @@ -0,0 +1,79 @@ +# -*- 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. diff --git a/doc/org/index.org b/doc/org/index.org index bffc627ae..53eb4fc59 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -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. diff --git a/doc/org/tools.org b/doc/org/tools.org index 81acd065c..9b1ccd10e 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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