adl.bib

@inproceedings{baarir.04.mascots,
  author = {Souheib Baarir and Jean-Michel Ili{\'e} and Alexandre
		  Duret-Lutz},
  title = {Improving Reachability Analysis for Partially Symmetric
		  High Level Petri Nets},
  booktitle = {Proceedings of the Poster Session of the 12th IEEE/ACM
		  International Symposium on Modeling, Analysis, and
		  Simulation of Computer and Telecommunication Systems
		  (MASCOTS'04)},
  editors = {Pete Harrison and Doug DeGroot},
  year = {2004},
  address = {Volendam, The Netherlands},
  month = oct,
  pages = {5--8},
  pdf = {adl/baarir.04.mascots.pdf},
  poster = {adl/baarir.04.mascots.poster.pdf},
  doi = {10.1109/MASCOT.2004.6}
}
@techreport{baarir.06.tr03,
  author = {Souheib Baarir and Alexandre Duret-Lutz},
  title = {Emptiness Check of Powerset {B\"u}chi Automata},
  institution = {Universit{\'e} Pierre et Marie Curie, LIP6-CNRS},
  year = {2006},
  type = {Technical report},
  number = {2006/003},
  address = {Paris, France},
  month = oct,
  pdf = {adl/baarir.06.tr03.pdf},
  abstract = {A possible attack on the state explosion of the
		  automata-theoretic approach to model-checking is to build
		  an automaton B whose states represent sets of states of the
		  original automaton A to check for emptiness. This paper
		  introduces two emptiness checks for B{\"u}chi automata
		  whose states represent sets that may include each other.
		  The first check on B is equivalent to a traditional
		  emptiness check on A but uses inclusion tests to direct and
		  further reduce the on-the-fly construction of B. The second
		  check is impressively faster but may return false
		  negatives. We illustrate and benchmark both using a
		  symmetry-based reduction.}
}
@inproceedings{baarir.07.acsd,
  author = {Souheib Baarir and Alexandre Duret-Lutz},
  title = {Emptiness Check of Powerset {B\"u}chi Automata},
  booktitle = {Proceedings of the 7th International Conference on
		  Application of Concurrency to System Design (ACSD'07)},
  editors = {Twan Basten and Gabriel Juh{\'a}s and Sandeep Shukla},
  year = {2007},
  month = jul,
  pages = {41--50},
  publisher = {IEEE Computer Society},
  pdf = {adl/baarir.07.acsd.pdf},
  slides = {adl/baarir.07.acsd.slides.pdf},
  abstract = {We introduce two emptiness checks for B{\"u}chi automata
		  whose states represent sets that may include each other.
		  The first is equivalent to a traditional emptiness check
		  but uses inclusion tests to direct the on-the-fly
		  construction of the automaton. The second is impressively
		  faster but may return false negatives. We illustrate and
		  benchmark the improvement on a symmetry-based reduction.},
  doi = {10.1109/ACSD.2007.49}
}
@inproceedings{baarir.07.msr,
  author = {Souheib Baarir and Alexandre Duret-Lutz},
  title = {Test de vacuit{\'e} pour automates de {B\"u}chi
		  ensemblistes avec tests d'inclusion},
  booktitle = {Actes du 6e Colloque Francophone sur la Mod{\'e}lisation
		  des Syst{\`e}mes R{\'e}actifs (MSR'07)},
  editors = {Jean-Michel Muller and {\'E}ric Niel and Laurent
		  Pi{\'e}trac},
  publisher = {Hermes-Lavoisier},
  year = {2007},
  month = oct,
  pages = {19--34},
  abstract = {Nous pr{\'e}sentons deux algorithmes d'emptiness check
		  pour les automates de B{\"u}chi dont les {\'e}tats sont des
		  ensembles qui peuvent s'inclure les uns les autres. Le
		  premier est {\'e}quivalent {\`a} un emptiness check
		  traditionnel, mais utilise des tests d'inclusion pour
		  diriger la construction {\`a} la vol{\'e}e de l'automate.
		  Le second est beaucoup plus rapide, mais peut retourner de
		  faux n{\'e}gatifs. Nous illustrons et {\'e}valuons
		  l'am{\'e}lioration avec une r{\'e}duction bas{\'e}e sur les
		  sym{\'e}tries.}
}
@inproceedings{baarir.14.forte,
  author = {Souheib Baarir and Alexandre Duret-Lutz},
  title = {Mechanizing the Minimization of Deterministic Generalized
		  {B\"u}chi Automata},
  booktitle = {Proceedings of the 34th IFIP International Conference on
		  Formal Techniques for Distributed Objects, Components and
		  Systems (FORTE'14)},
  year = {2014},
  month = jun,
  pages = {266--283},
  publisher = {Springer},
  pdf = {adl/baarir.14.forte.pdf},
  slides = {adl/baarir.14.forte.slides.pdf},
  series = {Lecture Notes in Computer Science},
  volume = {8461},
  abstract = {Deterministic B{\"u}chi automata (DBA) are useful to
		  (probabilistic) model checking and synthesis. We survey
		  techniques used to obtain and minimize DBAs for different
		  classes of properties. We extend these techniques to
		  support DBA that have generalized and transition-based
		  acceptance (DTGBA) as they can be even smaller. Our
		  minimization technique---a reduction to a SAT
		  problem---synthesizes a DTGBA equivalent to the input DTGBA
		  for any given number of states and number of acceptance
		  sets (assuming such automaton exists). We present
		  benchmarks using a framework that implements all these
		  techniques.},
  doi = {10.1007/978-3-662-43613-4_17}
}
@inproceedings{baarir.15.lpar,
  author = {Souheib Baarir and Alexandre Duret-Lutz},
  booktitle = {Proceedings of the 20th International Conference on Logic
		  for Programming, Artificial Intelligence, and Reasoning
		  (LPAR-20)},
  title = {{SAT}-based Minimization of Deterministic
		  $\omega$-Automata},
  year = {2015},
  month = nov,
  pages = {79--87},
  publisher = {Springer},
  volume = {9450},
  series = {Lecture Notes in Computer Science},
  abstract = {We describe a tool that inputs a deterministic
		  $\omega$-automaton with any acceptance condition, and
		  synthesizes an equivalent $\omega$-automaton with another
		  arbitrary acceptance condition and a given number of
		  states, if such an automaton exists. This tool, that relies
		  on a SAT-based encoding of the problem, can be used to
		  provide minimal $\omega$-automata equivalent to given
		  properties, for different acceptance conditions.},
  pdf = {adl/baarir.15.lpar.pdf},
  doi = {10.1007/978-3-662-48899-7_6}
}
@inproceedings{babiak.13.spin,
  author = {Tom{\'a}{\v{s}} Babiak and Thomas Badie and Alexandre
		  Duret-Lutz and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Jan
		  Strej{\v{c}}ek},
  title = {Compositional Approach to Suspension and Other
		  Improvements to {LTL} Translation},
  booktitle = {Proceedings of the 20th International SPIN Symposium on
		  Model Checking of Software (SPIN'13)},
  year = 2013,
  volume = {7976},
  series = {Lecture Notes in Computer Science},
  pages = {81--98},
  month = jul,
  publisher = {Springer},
  abstract = {Recently, there was defined a fragment of LTL (containing
		  fairness properties among other interesting formulae) whose
		  validity over a given infinite word depends only on an
		  arbitrary suffix of the word. Building upon an existing
		  translation from LTL to B{\"u}chi automata, we introduce a
		  compositional approach where subformulae of this fragment
		  are translated separately from the rest of an input formula
		  and the produced automata are composed in a way that the
		  subformulae are checked only in relevant accepting strongly
		  connected components of the final automaton. Further, we
		  suggest improvements over some procedures commonly applied
		  to generalized B{\"u}chi automata, namely over generalized
		  acceptance simplification and over degeneralization.
		  Finally we show how existing simulation-based reductions
		  can be implemented in a signature-based framework in a way
		  that improves the determinism of the automaton.},
  pdf = {adl/babiak.13.spin.pdf},
  slides = {adl/babiak.13.spin.slides.pdf},
  doi = {10.1007/978-3-642-39176-7_6}
}
@inproceedings{babiak.15.cav,
  author = {Tom{\'{a}\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and
		  Alexandre Duret-Lutz and Joachim Klein and Jan K{\v
		  r}et{\'{\i}}nsk{\'{y}} and David M{\"u}ller and David
		  Parker and Jan Strej{\v{c}}ek},
  title = {The {H}anoi {O}mega-{A}utomata Format},
  booktitle = {Proceedings of the 27th International Conference on
		  Computer Aided Verification (CAV'15)},
  year = 2015,
  volume = {9206},
  series = {Lecture Notes in Computer Science},
  pages = {479--486},
  month = jul,
  publisher = {Springer},
  abstract = { We propose a flexible exchange format for
		  $\omega$-automata, as typically used in formal
		  verification, and implement support for it in a range of
		  established tools. Our aim is to simplify the interaction
		  of tools, helping the research community to build upon
		  other people's work. A key feature of the format is the use
		  of very generic acceptance conditions, specified by Boolean
		  combinations of acceptance primitives, rather than being
		  limited to common cases such as B\"uchi, Streett, or Rabin.
		  Such flexibility in the choice of acceptance conditions can
		  be exploited in applications, for example in probabilistic
		  model checking, and furthermore encourages the development
		  of acceptance-agnostic tools for automata manipulations.
		  The format allows acceptance conditions that are either
		  state-based or transition-based, and also supports
		  alternating automata.},
  doi = {10.1007/978-3-319-21690-4_31},
  pdf = {adl/babiak.15.cav.pdf},
  poster = {adl/babiak.15.cav.poster.pdf},
  slides = {adl/babiak.15.cav.slides.pdf}
}
@incollection{barnat.18.hpcr,
  author = {Jiri Barnat and Vincent Bloemen and Alexandre Duret-Lutz
                  and Alfons Laarman and Laure Petrucci and Jaco van de Pol
                  and Etienne Renault},
  editor = {Youssef Hamadi and Lakhdar Sais},
  title = {Parallel Model Checking Algorithms for Linear-Time
                  Temporal Logic},
  booktitle = {Handbook of Parallel Constraint Reasoning},
  year = {2018},
  publisher = {Springer International Publishing},
  address = {Cham},
  chapter = 12,
  pages = {457--507},
  abstract = {Model checking is a fully automated, formal method for
                  demonstrating absence of bugs in reactive systems. Here,
                  bugs are violations of properties in Linear-time Temporal
                  Logic (LTL). A fundamental challenge to its application is
                  the exponential explosion in the number of system states.
                  The current chapter discusses the use of parallelism in
                  order to overcome this challenge. We reiterate the textbook
                  automata-theoretic approach, which reduces the model
                  checking problem to the graph problem of finding cycles. We
                  discuss several parallel algorithms that attack this
                  problem in various ways, each with different
                  characteristics: Depth-first search (DFS) based algorithms
                  rely on heuristics for good parallelization, but exhibit a
                  low complexity and good on-the-fly behavior. Breadth-first
                  search (BFS) based approaches, on the other hand, offer
                  good parallel scalability and support distributed
                  parallelism. In addition, we present various simpler model
                  checking tasks, which still solve a large and important
                  subset of the LTL model checking problem, and show how
                  these can be exploited to yield more efficient algorithms.
                  In particular, we provide simplified DFS-based search
                  algorithms and show that the BFS-based algorithms exhibit
                  optimal runtimes in certain cases.},
  isbn = {978-3-319-63516-3},
  doi = {10.1007/978-3-319-63516-3_12},
  pdf = {adl/barnat.18.hpcr.pdf}
}
@inproceedings{bensalem.11.sumo,
  author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
		  Fabrice Kordon},
  title = {Generalized {B\"u}chi Automata versus Testing Automata for
		  Model Checking},
  booktitle = {Proceedings of the second International Workshop on
		  Scalable and Usable Model Checking for Petri Net and other
		  models of Concurrency (SUMO'11)},
  address = {Newcastle, UK},
  year = {2011},
  month = jun,
  volume = {726},
  publisher = {CEUR},
  series = {Workshop Proceedings},
  pdf = {adl/bensalem.11.sumo.pdf},
  abstract = {Geldenhuys and Hansen have shown that a kind of
		  $\omega$-automaton known as \emph{testing automata} can
		  outperform the B{\"u}chi automata traditionally used in the
		  automata-theoretic approach to model checking. This work
		  completes their experiments by including a comparison with
		  generalized B{\"u}chi automata; by using larger state
		  spaces derived from Petri nets; and by distinguishing
		  violated formul\ae{} (for which testing automata fare
		  better) from verified formul\ae{} (where testing automata
		  are hindered by their two-pass emptiness check).}
}
@article{bensalem.12.topnoc,
  author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
		  Fabrice Kordon},
  title = {Model Checking using Generalized Testing Automata},
  journal = {Transactions on Petri Nets and Other Models of Concurrency
		  (ToPNoC VI)},
  volume = 7400,
  series = {Lecture Notes in Computer Science},
  year = 2012,
  publisher = {Springer},
  pages = {94--112},
  pdf = {adl/bensalem.12.topnoc.pdf},
  abstract = {Geldenhuys and Hansen showed that a kind of
		  $\omega$-automata known as \emph{Testing Automata} (TA)
		  can, in the case of stuttering-insensitive properties,
		  outperform the B{\"u}chi automata traditionally used in the
		  automata-theoretic approach to model checking. \par In
		  previous work, we compared TA against
		  \emph{Transition-based Generalized B{\"u}chi Automata}
		  (TGBA), and concluded that TA were more interesting when
		  counterexamples were expected, otherwise TGBA were more
		  efficient. \par In this work we introduce a new kind of
		  automata, dubbed \emph{Transition-based Generalized Testing
		  Automata} (TGTA), that combine ideas from TA and TGBA.
		  Implementation and experimentation of TGTA show that they
		  outperform other approaches in most of the cases.},
  doi = {10.1007/978-3-642-35179-2_5}
}
@inproceedings{bensalem.14.tacas,
  author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
		  Fabrice Kordon and Yann Thierry-Mieg},
  title = {Symbolic Model Checking of Stutter Invariant Properties
		  Using Generalized Testing Automata},
  booktitle = {Proceedings of the 20th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'14)},
  year = {2014},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {8413},
  pages = {440--454},
  address = {Grenoble, France},
  month = apr,
  abstract = {In a previous work, we showed that a kind of
		  $\omega$-automata known as \emph{Tran\-sition-based
		  Generalized Testing Automata} (TGTA) can outperform the
		  B{\"u}chi automata traditionally used for \textit{explicit}
		  model checking when verifying stutter-invariant properties.
		  In this work, we investigate the use of these generalized
		  testing automata to improve \textit{symbolic} model
		  checking of stutter-invariant LTL properties. We propose an
		  efficient symbolic encoding of stuttering transitions in
		  the product between a model and a TGTA. Saturation
		  techniques available for decision diagrams then benefit
		  from the presence of stuttering self-loops on all states of
		  TGTA. Experimentation of this approach confirms that it
		  outperforms the symbolic approach based on
		  (transition-based) Generalized B{\"u}chi Automata.},
  pdf = {adl/bensalem.14.tacas.pdf},
  doi = {10.1007/978-3-642-54862-8_38}
}
@inproceedings{blahoudek.14.spin,
  author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Mojm\'{i}r K\v{r}et\'{i}nsk\'{y} and Jan Strej\v{c}ek},
  title = {Is There a Best {B\"u}chi Automaton for Explicit Model
		  Checking?},
  booktitle = {Proceedings of the 21th International SPIN Symposium on
		  Model Checking of Software (SPIN'14)},
  year = {2014},
  publisher = {ACM},
  pages = {68--76},
  month = jul,
  abstract = {LTL to B{\"u}chi automata (BA) translators are
		  traditionally optimized to produce automata with a small
		  number of states or a small number of non-deterministic
		  states. In this paper, we search for properties of
		  B{\"u}chi automata that really influence the performance of
		  explicit model checkers. We do that by manual analysis of
		  several automata and by experiments with common LTL-to-BA
		  translators and realistic verification tasks. As a result
		  of these experiences, we gain a better insight into the
		  characteristics of automata that work well with Spin.},
  pdf = {adl/blahoudek.14.spin.pdf},
  doi = {10.1145/2632362.2632377}
}
@inproceedings{blahoudek.15.spin,
  author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Vojt\v{c}ech Rujbr and Jan Strej\v{c}ek},
  title = {On Refinement of {B\"u}chi Automata for Explicit Model
		  Checking},
  booktitle = {Proceedings of the 22th International SPIN Symposium on
		  Model Checking of Software (SPIN'15)},
  year = 2015,
  pages = {66--83},
  month = aug,
  series = {Lecture Notes in Computer Science},
  volume = 9232,
  publisher = {Springer},
  abstract = {In explicit model checking, systems are typically
		  described in an implicit and compact way. Some valid
		  information about the system can be easily derived directly
		  from this description, for example that some atomic
		  propositions cannot be valid at the same time. The paper
		  shows several ways to apply this information to improve the
		  B{\"u}chi automaton built from an LTL specification. As a
		  result, we get smaller automata with shorter edge labels
		  that are easier to understand and, more importantly, for
		  which the explicit model checking process performs better.},
  pdf = {adl/blahoudek.15.spin.pdf},
  doi = {10.1007/978-3-319-23404-5_6}
}
@inproceedings{blahoudek.17.lpar,
  author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Mikul\'{a}\v{s} Kloko\v{c}ka and Mojm\'{\i}r
		  K\v{r}et\'{\i}nsk\'{y} and Jan Strej\v{c}ek},
  title = {Seminator: A Tool for Semi-Determinization of
		  Omega-Automata},
  booktitle = {Proceedings of the 21th International Conference on Logic
		  for Programming, Artificial Intelligence, and Reasoning
		  (LPAR-21)},
  year = {2017},
  editor = {Thomas Eiter and David Sands and Geoff Sutcliffe},
  volume = {46},
  series = {EPiC Series in Computing},
  pages = {356--367},
  month = may,
  publisher = {EasyChair Publications},
  pdf = {adl/blahoudek.17.lpar.pdf},
  abstract = {We present a tool that transforms nondeterministic
		  $\omega$-automata to semi-deterministic $\omega$-automata.
		  The tool Seminator accepts transition-based generalized
		  B\"uchi automata (TGBA) as an input and produces automata
		  with two kinds of semi-determinism. The implemented
		  procedure performs degeneralization and
		  semi-determinization simultaneously and employs several
		  other optimizations. We experimentally evaluate Seminator
		  in the context of LTL to semi-deterministic automata
		  translation.}
}
@inproceedings{bloemen.17.spin,
  author = {Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de
		  Pol},
  title = {Explicit State Model Checking with Generalized {B\"u}chi and
		  {R}abin Automata},
  booktitle = {Proceedings of the 24th International SPIN Symposium on Model
		  Checking of Software (SPIN'17)},
  pages = {50--59},
  year = {2017},
  publisher = {ACM},
  month = jul,
  pdf = {adl/bloemen.17.spin.pdf},
  doi = {10.1145/3092282.3092288},
  abstract = {In the automata theoretic approach to explicit state LTL
		  model checking, the synchronized product of the model and
		  an automaton that represents the negated formula is checked
		  for emptiness. In practice, a (transition-based
		  generalized) B\"uchi automaton (TGBA) is used for this
		  procedure.

		  This paper investigates whether using a more general form
		  of acceptance, namely transition-based generalized Rabin
		  automata (TGRAs), improves the model checking procedure.
		  TGRAs can have significantly fewer states than TGBAs,
		  however the corresponding emptiness checking procedure is
		  more involved. With recent advances in probabilistic model
		  checking and LTL to TGRA translators, it is only natural to
		  ask whether checking a TGRA directly is more advantageous
		  in practice.

		  We designed a multi-core TGRA checking algorithm and
		  performed experiments on a subset of the models and
		  formulas from the 2015 Model Checking Contest. We observed
		  that our algorithm can be used to replace a TGBA checking
		  algorithm without losing performance. In general, we found
		  little to no improvement by checking TGRAs directly.}
}
@inproceedings{burrus.03.mpool,
  author = {Nicolas Burrus and Alexandre Duret-Lutz and Thierry
		  G\'eraud and David Lesage and Rapha\"el Poss},
  title = {A Static {C++} Object-Oriented Programming (SCOOP)
		  Paradigm Mixing Benefits of Traditional OOP and Generic
		  Programming},
  booktitle = {Proceedings of the Workshop on Multiple Paradigm with OO
		  Languages (MPOOL'03)},
  year = {2003},
  address = {Anaheim, California},
  month = oct,
  pdf = {adl/burrus.03.mpool.pdf},
  proceedings = {http://www.fz-juelich.de/nic-series/volume27/volume27.html},
  abstract = {Object-oriented and generic programming are both supported
		  in C++. OOP provides high expressiveness whereas GP leads
		  to more efficient programs by avoiding dynamic typing. This
		  paper presents SCOOP, a new paradigm which enables both
		  classical OO design and high performance in C++ by mixing
		  OOP and GP. We show how classical and advanced OO features
		  such as virtual methods, multiple inheritance, argument
		  covariance, virtual types and multimethods can be
		  implemented in a fully statically typed model, hence
		  without run-time overhead.}
}
@techreport{clouard.99.tr,
  author = {R\'egis Clouard and Abderrahim Elmoataz and Fran\c{c}ois
		  Angot and Olivier Lezoray and Alexandre Duret-Lutz},
  title = {Une biblioth\`eque et un environnement de programmation
		  d'op\'erateurs de traitement d'images},
  institution = {GREYC-ISMRA},
  year = {1999},
  number = {99008},
  address = {Caen, France},
  month = nov,
  url = {http://www.greyc.ismra.fr/~regis/Pandore/}
}
@inproceedings{couvreur.05.spin,
  author = {Jean-Michel Couvreur and Alexandre Duret-Lutz and Denis
		  Poitrenaud},
  title = {On-the-Fly Emptiness Checks for Generalized {B\"u}chi
		  Automata},
  booktitle = {Proceedings of the 12th International SPIN Workshop on
		  Model Checking of Software},
  pages = {143--158},
  year = {2005},
  editor = {Patrice Godefroid},
  volume = {3639},
  series = {Lecture Notes in Computer Science},
  month = aug,
  publisher = {Springer},
  pdf = {adl/couvreur.05.spin.draft.pdf},
  slides = {adl/couvreur.05.spin.slides.pdf},
  abstract = { Emptiness check is a key operation in the
		  automata-theoretic approach to LTL verification. However,
		  it is usually done on B{\"u}chi automata with a single u
		  acceptance condition. We review existing on-the-fly
		  emptiness-check algorithms for generalized B{\"u}chi
		  automata (i.e., with multiple acceptance conditions) and u
		  show how they compete favorably with emptiness-checks for
		  degeneralized automata, especially in presence of weak
		  fairness assumptions. We also introduce a new
		  emptiness-check algorithm, some heuristics to improve
		  existing checks, and propose algorithms to compute
		  accepting runs in the case of multiple acceptance
		  conditions. },
  doi = {10.1007/11537328_15}
}
@inproceedings{darbon.02.ismm,
  author = {J\'er\^ome Darbon and Thierry G\'eraud and Alexandre
		  Duret-Lutz},
  title = {Generic Implementation of Morphological Image Operators},
  booktitle = {Mathematical Morphology, Proceedings of the 6th
		  International Symposium (ISMM)},
  pages = {175--184},
  year = {2002},
  address = {Sydney, Australia},
  month = apr,
  publisher = {Sciro Publishing},
  pdf = {adl/darbon.02.ismm.pdf},
  abstract = { Several libraries dedicated to mathematical morphology
		  exist. But they lack genericity, that is to say, the
		  ability for operators to accept input of different
		  natures---2D binary images, graphs enclosing floating
		  values, etc. We describe solutions which are integrated in
		  Olena, a library providing morphological operators. We
		  demonstrate with some examples that translating
		  mathematical formulas and algorithms into source code is
		  made easy and safe with Olena. Moreover, experimental
		  results show that no extra costs at run-time are induced.
		  }
}
@inproceedings{demaille.08.fsmnlp,
  author = {Akim Demaille and Alexandre Duret-Lutz and Florian Lesaint
		  and Sylvain Lombardy and Jacques Sakarovitch and Florent
		  Terrones},
  title = {An {XML} format proposal for the description of weighted
		  automata, transducers, and regular expressions},
  booktitle = {Proceedings of the seventh international workshop on
		  Finite-State Methods and Natural Language Processing
		  (FSMNLP'08)},
  year = {2008},
  address = {Ispra, Italia},
  month = sep,
  abstract = {We present an XML format that allows to describe a large
		  class of finite weighted automata and transducers. Our
		  design choices stem from our policy of making the
		  implementation as simple as possible. This format has been
		  tested for the communication between the modules of our
		  automata manipulation platform Vaucanson, but this document
		  is less an experiment report than a position paper intended
		  to open the discussion among the community of automata
		  software writers.},
  pdf = {adl/demaille.08.fsmnlp.pdf}
}
@inproceedings{demaille.13.ciaa,
  author = {Akim Demaille and Alexandre Duret-Lutz and Sylvain
		  Lombardy and Jacques Sakarovitch},
  title = {Implementation Concepts in {V}aucanson 2},
  booktitle = {Proceedings of Implementation and Application of Automata,
		  18th International Conference (CIAA'13)},
  pages = {96--107},
  year = 2013,
  editor = {Oscar H. Ibarra and Zhe Dang},
  publisher = {Springer},
  volume = 2759,
  series = {Lecture Notes in Computer Science},
  address = {Santa Barbara, CA, USA},
  month = jul,
  project = {Vaucanson},
  abstract = {Vaucanson is an open source C++ platform dedicated to the
		  computation with finite weighted automata. It is generic:
		  it allows to write algorithms that apply on a wide set of
		  mathematical objects. Initiated ten years ago, several
		  shortcomings were discovered along the years, especially
		  problems related to code complexity and obfuscation as well
		  as performance issues. This paper presents the concepts
		  underlying Vaucanson 2, a complete rewrite of the platform
		  that addresses these issues.},
  pdf = {adl/demaille.13.ciaa.pdf},
  doi = {10.1007/978-3-642-39274-0_12}
}
@inproceedings{demaille.14.ciaa,
  author = {Akim Demaille and Alexandre Duret-Lutz and Sylvain
		  Lombardy and Luca Saiu and Jacques Sakarovitch},
  title = {A Type System for Weighted Automata and Rational
		  Expressions},
  booktitle = {Proceedings of Implementation and Application of Automata,
		  19th International Conference (CIAA'14)},
  year = 2014,
  fixmepublisher = {Springer},
  fixmeseries = {Lecture Notes in Computer Science},
  address = {Giessen, Germany},
  month = jul,
  abstract = {We present a type system for automata and rational
		  expressions, expressive enough to encompass weighted
		  automata and transducers in a single coherent formalism.
		  The system allows to express useful properties about the
		  applicability of operations including binary heterogeneous
		  functions over automata.\\ We apply the type system to the
		  design of the Vaucanson platform, a library dedicated to
		  the computation with finite weighted automata, in which
		  genericity and high efficiency are obtained at the lowest
		  level through the use of template metaprogramming, by
		  letting the template system play the role of a static type
		  system for automata. Between such a low-level layer and the
		  interactive high-level interface, the type system plays the
		  crucial role of a mediator and allows for a
		  cleanly-structured use of dynamic compilation. },
  pdf = {adl/demaille.14.ciaa.pdf},
  doi = {10.1007/978-3-319-08846-4_12}
}
@inproceedings{duret.00.gcseyrw,
  author = {Alexandre Duret-Lutz},
  title = {Olena: a Component-Based Platform for Image Processing,
		  mixing Generic, Generative and {OO} Programming},
  booktitle = {Proceedings of 2nd International Symposium on Generative
		  and Component-Based Software Engineering (GCSE 2000)},
  publisher = {Young Researchers Workshop (published in
		  ``Net.ObjectDays2000'')},
  year = {2000},
  address = {Erfurt, Germany},
  pages = {653--659},
  month = oct,
  url = {http://www.lrde.epita.fr/dload/papers/gcse00-yrw/olena.html}
}
@techreport{duret.00.tr01,
  author = {Alexandre Duret-Lutz and Thierry G{\'e}raud},
  title = {Improving Object-Oriented Generic Programming},
  institution = {EPITA Research and Development Laboratory},
  year = {2000},
  type = {Technical Report},
  number = {0001},
  address = {Paris},
  month = apr,
  pdf = {adl/duret.00.tr01.pdf},
  abstract = { Great efforts have gone into building scientific
		  libraries dedicated to particular application domains and a
		  main issue is to manage the large number of data types
		  involved in a given domain. An ideal algorithm
		  mplementation should be general: it should be written once
		  and process data in an abstract way. Moreover, it should be
		  efficient. For several years, some libraries have been
		  using generic programming to address this problem. In this
		  report, we present two major improvements of this paradigm.
		  \par In generic libraries, a concept is the description of
		  a set of requirements on a type that parameterizes an
		  algorithm implementation (the notion of concept replaces
		  the classical object-oriented notion of abstract class). A
		  problem is that, until now, concepts are only defined in
		  the documentation. We managed to make them explicit in the
		  program by representing a concept by a type; moreover,
		  (multiple) concept inheritance is fully supported. The
		  procedure signature thus evolves from \texttt{void
		  foo(AbstractA\&)} for classic object-orientation, and from
		  \texttt{template void foo(A\&)} for classic
		  generic programming, towards \texttt{template void
		  foo(ConceptA\&)}. This results in a better support of
		  procedure overloading, which is of prime importance for
		  libraries where each algorithm implementation can have
		  numerous variations. \par Another problem is that the
		  generic programming paradigm suffers from a lack of
		  appropriate design patterns. We observed that classical
		  patterns of Gamma et al. can be translated into this
		  paradigm while handling operation polymorphism by
		  parametric polymorphism. In these patterns, method calls
		  can be solved statically, because the inferior type of each
		  object in generic programming is known at compile-time. We
		  thus preserve their modularity and reusability properties
		  but we avoid the performance penalty due to their dynamic
		  behavior, which is a critical issue in numerical computing.
		  This results in better design capabilities for
		  object-oriented generic libraries. }
}
@inproceedings{duret.01.ae,
  author = {Alexandre Duret-Lutz},
  title = {Expression Templates in {Ada}},
  booktitle = {Proceedings of the 6th International Conference on
		  Reliable Software Technologies (Ada-Europe'01)},
  year = {2001},
  address = {Leuven, Belgium},
  month = may,
  pages = {191--202},
  volume = {2043},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  note = {Best paper award.},
  pdf = {adl/duret.01.ae.pdf},
  abstract = {High-order matrix or vector expressions tend to be
		  penalized by the use of huge temporary variables.
		  Expression templates is a C++ technique which can be used
		  to avoid these temporaries, in a way that is transparent to
		  the user. We present an Ada adaptation of this technique
		  which---while not transparent---addresses the same
		  efficiency issue as the original. We make intensive use of
		  the signature idiom to combine packages together, and
		  discuss its importance in generic programming. Finally, we
		  express some concerns about generic programming in Ada.},
  doi = {10.1007/3-540-45136-6_15}
}
@inproceedings{duret.01.coots,
  author = {Alexandre Duret-Lutz and Thierry G\'eraud and Akim
		  Demaille},
  title = {Design Patterns for Generic Programming in {C++}},
  booktitle = {Proceedings of the 6th USENIX Conference on
		  Object-Oriented Technologies and Systems (COOTS'01)},
  year = {2001},
  address = {San Antonio, Texas, USA},
  month = jan,
  pages = {189--202},
  publisher = {USENIX Association},
  pdf = {adl/duret.01.coots.pdf},
  url = {http://www.usenix.org/publications/library/proceedings/coots01/duret.html},
  abstract = {Generic programming is a paradigm whose wide adoption by
		  the C++ community is quite recent. In this scheme most
		  classes and procedures are parameterized, leading to the
		  construction of general and efficient software components.
		  In this paper, we show how some design patterns from Gamma
		  et al. can be adapted to this paradigm. Although these
		  patterns rely highly on dynamic binding, we show that, by
		  intensive use of parametric polymorphism, the method calls
		  in these patterns can be resolved at compile-time. In
		  intensive computations, the generic patterns bring a
		  significant speed-up compared to their classical peers. }
}
@mastersthesis{duret.03.msc,
  author = {Alexandre Duret-Lutz and Rachid Rebiha},
  title = {SPOT\,: une biblioth{\`e}que de v{\'e}rification de
		  propri{\'e}t{\'e}s de logique temporelle {\`a} temps
		  lin{\'e}aire},
  school = {DEA Syst{\`e}mes Informatiques R{\'e}partis,
		  Universit{\'e} de Paris 6},
  month = sep,
  year = {2003},
  pdf = {adl/duret.03.msc.pdf}
}
@inproceedings{duret.04.mascots,
  author = {Alexandre Duret-Lutz and Denis Poitrenaud},
  title = {SPOT: an Extensible Model Checking Library using
		  Transition-based Generalized {B\"u}chi Automata},
  booktitle = {Proceedings of the 12th IEEE/ACM International Symposium
		  on Modeling, Analysis, and Simulation of Computer and
		  Telecommunication Systems (MASCOTS'04)},
  editors = {Doug DeGroot and Pete Harrison},
  year = {2004},
  address = {Volendam, The Netherlands},
  month = oct,
  publisher = {IEEE Computer Society},
  pages = {76--83},
  pdf = {adl/duret.04.mascots.draft.pdf},
  abstract = { Spot is a C++ library offering model checking bricks that
		  can be combined and interfaced with third party tools to
		  build a model checker. It relies on Transition-based
		  Generalized B{\"u}chi Automata (TGBA) and does not need to
		  degeneralize these automata to check their emptiness. We
		  motivate the choice of TGBA by illustrating a very simple
		  (yet efficient) translation of LTL into TGBA. We then show
		  how it supports on-the-fly computations, and how it can be
		  extended or integrated in other tools. },
  doi = {10.1109/MASCOT.2004.1348184}
}
@phdthesis{duret.07.phd,
  author = {Alexandre Duret-Lutz},
  title = {Contributions {\`a} l'approche automate pour la
		  v{\'e}rification de propri{\'e}t{\'e}s de syst{\`e}mes
		  concurrents},
  school = {Universit{\'e} Pierre et Marie Curie (Paris 6)},
  year = {2007},
  month = jul,
  pdf = {adl/duret.07.phd.pdf},
  slides = {adl/duret.07.phd.slides.pdf},
  www = {../th.html}
}
@inproceedings{duret.09.atva,
  author = {Alexandre Duret-Lutz and Denis Poitrenaud and Jean-Michel
		  Couvreur},
  title = {On-the-fly Emptiness Check of Transition-based {S}treett
		  Automata},
  booktitle = {Proceedings of the 7th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'09)},
  year = {2009},
  editor = {Zhiming Liu and Anders P. Ravn},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {213--227},
  volume = {5799},
  pdf = {adl/duret.09.atva.pdf},
  slides = {adl/duret.09.atva.slides.pdf},
  abstract = {In the automata theoretic approach to model checking,
		  checking a state-space $S$ against a linear-time property
		  $\varphi$ can be done in $\mathrm{O}(|S|\times
		  2^{\mathrm{O}(|\varphi|)})$ time. When model checking under
		  $n$ strong fairness hypotheses expressed as a Generalized
		  B\"uchi automaton, this complexity becomes
		  $\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.\par
		  Here we describe an algorithm to check the emptiness of
		  Streett automata, which allows model checking under $n$
		  strong fairness hypotheses in $\mathrm{O}(|S|\times
		  2^{\mathrm{O}(|\varphi|)}\times n)$. We focus on
		  transition-based Streett automata, because it allows us to
		  express strong fairness hypotheses by injecting Streett
		  acceptance conditions into the state-space without any blowup.},
  doi = {10.1007/978-3-642-04761-9_17}
}
@techreport{duret.11.arxiv,
  author = {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
		  and Yann Thierry-Mieg},
  title = {Combining Explicit and Symbolic Approaches for Better
		  On-the-Fly {LTL} Model Checking},
  institution = {arXiv},
  year = 2011,
  number = {1106.5700},
  month = jun,
  note = {Extended version of our ATVA'11 paper, presenting two new
		  techniques instead of one.},
  url = {http://arxiv.org/abs/1106.5700},
  pdf = {adl/duret.11.arxiv.pdf},
  abstract = {We present two new hybrid techniques that replace the
		  synchronized product used in the automata-theoretic
		  approach for LTL model checking. The proposed products are
		  explicit graphs of aggregates (symbolic sets of states)
		  that can be interpreted as B{\"u}chi automata. These hybrid
		  approaches allow on the one hand to use classical
		  emptiness-check algorithms and build the graph on-the-fly,
		  and on the other hand, to have a compact encoding of the
		  state space thanks to the symbolic representation of the
		  aggregates. The \emph{Symbolic Observation Product} assumes
		  a globally stuttering property (e.g., LTL-X) to aggregate
		  states. The \emph{Self-Loop Aggregation Product} does not
		  require the property to be globally stuttering (i.e., it
		  can tackle full LTL), but dynamically detects and exploits
		  a form of stuttering where possible. Our experiments show
		  that these two variants, while incomparable with each
		  other, can outperform other existing approaches.}
}
@inproceedings{duret.11.atva,
  author = {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
		  and Yann Thierry-Mieg},
  title = {Self-Loop Aggregation Product --- A New Hybrid Approach to
		  On-the-Fly {LTL} Model Checking},
  booktitle = {Proceedings of the 9th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'11)},
  year = {2011},
  series = {Lecture Notes in Computer Science},
  address = {Taipei, Taiwan},
  month = oct,
  publisher = {Springer},
  volume = {6996},
  pages = {336--350},
  abstract = {We present the \emph{Self-Loop Aggregation Product}
		  (SLAP), a new hybrid technique that replaces the
		  synchronized product used in the automata-theoretic
		  approach for LTL model checking. The proposed product is an
		  explicit graph of aggregates (symbolic sets of states) that
		  can be interpreted as a B{\"u}chi automata. The criterion
		  used by SLAP to aggregate states from the Kripke structure
		  is based on the analysis of self-loops that occur in the
		  B{\"u}chi automaton expressing the property to verify. Our
		  hybrid approach allows on the one hand to use classical
		  emptiness-check algorithms and build the graph on-the-fly,
		  and on the other hand, to have a compact encoding of the
		  state space thanks to the symbolic representation of the
		  aggregates. Our experiments show that this technique often
		  outperforms other existing (hybrid or fully symbolic)
		  approaches.},
  pdf = {adl/duret.11.atva.pdf},
  slides = {adl/duret.11.atva.slides.pdf},
  doi = {10.1007/978-3-642-24372-1_24}
}
@misc{duret.11.sumo,
  author = {Alexandre Duret-Lutz},
  title = {Building {LTL} Model Checkers using {T}ransition-based
		  {G}eneralized {B\"u}chi {A}utomata},
  howpublished = {Invited talk to SUMo'11},
  month = jun,
  year = {2011},
  slides = {adl/duret.11.sumo.slides.pdf}
}
@inproceedings{duret.11.vecos,
  author = {Alexandre Duret-Lutz},
  title = {{LTL} Translation Improvements in {Spot}},
  booktitle = {Proceedings of the 5th International Workshop on
		  Verification and Evaluation of Computer and Communication
		  Systems (VECoS'11)},
  year = {2011},
  series = {Electronic Workshops in Computing},
  address = {Tunis, Tunisia},
  month = sep,
  publisher = {British Computer Society},
  abstract = {Spot is a library of model-checking algorithms. This paper
		  focuses on the module translating LTL formul{\ae} into
		  automata. We discuss improvements that have been
		  implemented in the last four years, we show how Spot's
		  translation competes on various benchmarks, and we give
		  some insight into its implementation.},
  proceedings = {http://ewic.bcs.org/category/15853},
  pdf = {adl/duret.11.vecos.pdf},
  slides = {adl/duret.11.vecos.slides.pdf}
}
@misc{duret.12.ciaa,
  author = {Alexandre Duret-Lutz},
  title = {The {S}pot Library, and its Online Translator from {LTL}
		  (and {PSL}) to {B\"u}chi Automata},
  note = {Two-page flyer for the software demo session.},
  month = jul,
  year = {2012},
  howpublished = {Distributed in the CIAA'12 conference booklet, not in the
		  main proceedings},
  pdf = {adl/duret.12.ciaa.flyer.pdf}
}
@inproceedings{duret.13.atva,
  author = {Alexandre Duret-Lutz},
  title = {Manipulating {LTL} formulas using {Spot} 1.0},
  booktitle = {Proceedings of the 11th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'13)},
  year = 2013,
  series = {Lecture Notes in Computer Science},
  volume = {8172},
  pages = {442--445},
  address = {Hanoi, Vietnam},
  month = oct,
  publisher = {Springer},
  abstract = {We present a collection of command-line tools designed to
		  generate, filter, convert, simplify, lists of Linear-time
		  Temporal Logic formulas. These tools were introduced in the
		  release 1.0 of Spot, and we believe they should be of
		  interest to anybody who has to manipulate LTL formulas. We
		  focus on two tools in particular: ltlfilt, to filter and
		  transform formulas, and ltlcross to cross-check
		  LTL-to-B{\"u}chi-Automata translators.},
  pdf = {adl/duret.13.atva.pdf},
  slides = {adl/duret.13.atva.slides.pdf},
  doi = {10.1007/978-3-319-02444-8_31}
}
@article{duret.14.ijccbs,
  author = {Alexandre Duret-Lutz},
  title = {{LTL} Translation Improvements in {S}pot 1.0},
  journal = {International Journal on Critical Computer-Based Systems},
  year = {2014},
  volume = {5},
  number = {1/2},
  pages = {31--54},
  month = mar,
  pdf = {adl/duret.14.ijccbs.draft.pdf},
  abstract = { Spot is a library of model-checking algorithms started in
		  2003. This paper focuses on its module for translating
		  linear-time temporal logic (LTL) formulas into B{\"u}chi
		  automata: one of the steps required in the
		  automata-theoretic approach to LTL model-checking.

		  We detail the different algorithms involved in this
		  translation: the core translation itself, which performs
		  many simplifications thanks to its use of binary decision
		  diagrams; the pre-processing of the LTL formulas with
		  rewriting rules chosen to help their translation; and
		  various post-processing algorithms whose use depends on the
		  intent of the translation: do we favor deterministic
		  automata, or small automata?

		  Using different benchmarks, we show how Spot competes with
		  other LTL translators, and how it has improved over the
		  years.

		  \textbf{Note:} This is an extended version
		  of~\cite{duret.11.vecos}.},
  doi = {10.1504/IJCCBS.2014.059594}
}
@inproceedings{duret.16.atva,
  author = {Alexandre Duret-Lutz and Fabrice Kordon and Denis
		  Poitrenaud and Etienne Renault},
  title = {Heuristics for Checking Liveness Properties with Partial
		  Order Reductions},
  booktitle = {Proceedings of the 14th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'16)},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {9938},
  pages = {340--356},
  year = {2016},
  month = oct,
  pdf = {adl/duret.16.atva.pdf},
  abstract = {Checking liveness properties with partial-order reductions
		  requires a cycle proviso to ensure that an action cannot be
		  postponed forever. The proviso forces each cycle to contain
		  at least one fully expanded state. We present new
		  heuristics to select which state to expand, hoping to
		  reduce the size of the resulting graph. The choice of the
		  state to expand is done when encountering a
		  \emph{dangerous} edge. Almost all existing provisos expand
		  the source of this edge, while this paper also explores the
		  expansion of the destination and the use of SCC-based
		  information.},
  doi = {10.1007/978-3-319-46520-3_22}
}
@inproceedings{duret.16.atva2,
  author = {Alexandre Duret-Lutz and Alexandre Lewkowicz and Amaury
		  Fauchille and Thibaud Michaud and Etienne Renault and
		  Laurent Xu},
  title = {Spot 2.0 --- a framework for {LTL} and $\omega$-automata
		  manipulation},
  booktitle = {Proceedings of the 14th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'16)},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {9938},
  pages = {122--129},
  year = {2016},
  month = oct,
  pdf = {adl/duret.16.atva2.pdf},
  abstract = {We present Spot 2.0, a C++ library with Python bindings
		  and an assortment of command-line tools designed to
		  manipulate LTL and $\omega$-automata in batch. New
		  automata-manipulation tools were introduced in Spot 2.0;
		  they support arbitrary acceptance conditions, as
		  expressible in the Hanoi Omega Automaton format. Besides
		  being useful to researchers who have automata to process,
		  its Python bindings can also be used in interactive
		  environments to teach $\omega$-automata and model checking.},
  doi = {10.1007/978-3-319-46520-3_8}
}
@phdthesis{duret.17.hdr,
  author = {Alexandre Duret-Lutz},
  title = {Contributions to LTL and $\omega$-Automata for Model
		  Checking},
  school = {Universit{\'e} Pierre et Marie Curie (Paris 6)},
  year = {2017},
  month = feb,
  pdf = {adl/duret.17.hdr.pdf},
  slides = {adl/duret.17.hdr.slides.pdf},
  type = {Habilitation Thesis}
}
@techreport{duret.99.tr03,
  author = {Alexandre Duret-Lutz and Thierry G\'eraud},
  title = {Patrons de conception statiques pour la programmation
		  g\'en\'erique en {C++}},
  institution = {EPITA Research and Development Laboratory},
  year = {1999},
  type = {Technical Report},
  number = {9903},
  address = {Paris},
  month = sep,
  pdf = {adl/duret.99.tr03.pdf}
}
@inproceedings{fronc.13.atva,
  author = {{\L}ukasz Fronc and Alexandre Duret-Lutz},
  title = {{LTL} Model Checking with {N}eco},
  booktitle = {Proceedings of the 11th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'13)},
  year = 2013,
  series = {Lecture Notes in Computer Science},
  volume = {8172},
  pages = {451--454},
  address = {Hanoi, Vietnam},
  month = oct,
  publisher = {Springer},
  abstract = {We introduce neco-spot, an LTL model checker for Petri net
		  models. It builds upon Neco, a compiler turning Petri nets
		  into native shared libraries that allows fast on-the-fly
		  exploration of the state-space, and upon Spot, a C++
		  library of model-checking algorithms. We show the
		  architecture of Neco and explain how it was combined with
		  Spot to build an LTL model checker.},
  pdf = {adl/fronc.13.atva.pdf},
  slides = {adl/fronc.13.atva.slides.pdf},
  doi = {10.1007/978-3-319-02444-8_33}
}
@inproceedings{geraud.00.europlop,
  author = {Thierry G\'eraud and Alexandre Duret-Lutz},
  title = {Generic Programming Redesign of Patterns},
  booktitle = {Proceedings of the 5th European Conference on Pattern
		  Languages of Programs (EuroPLoP'00)},
  year = {2000},
  month = jul,
  page = {283--294},
  editor = {M. Devos and A. R\"uping},
  publisher = {UVK, Univ. Verlag, Konstanz},
  adress = {Irsee, Germany},
  pdf = {adl/geraud.00.europlop.pdf}
}
@inproceedings{geraud.00.icpr,
  author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz
		  and Dimitri Papadopoulos-Orfanos and Jean-Fran\c{c}ois
		  Mangin},
  title = {Obtaining Genericity for Image Processing and Pattern
		  Recognition Algorithms},
  booktitle = {Proceedings of the 15th International Conference on
		  Pattern Recognition (ICPR'00)},
  year = {2000},
  month = sep,
  address = {Barcelona, Spain},
  volume = {4},
  pages = {816--819},
  publisher = {IEEE Computer Society},
  abstract = { Algorithm libraries dedicated to image processing and
		  pattern recognition are not reusable; to run an algorithm
		  on particular data, one usually has either to rewrite the
		  algorithm or to manually "copy, paste, and modify". This is
		  due to the lack of genericity of the programming paradigm
		  used to implement the libraries. In this paper, we present
		  a recent paradigm that allows algorithms to be written once
		  and for all and to accept input of various types. Moreover,
		  this total reusability can be obtained with a very
		  comprehensive writing and without significant cost at
		  execution, compared to a dedicated algorithm. This new
		  paradigm is called "generic programming" and is fully
		  supported by the C++ language. We show how this paradigm
		  can be applied to image processing and pattern recognition
		  routines. The perspective of our work is the creation of a
		  generic library.}
}
@inproceedings{geraud.01.ai,
  author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz},
  title = {Applying Generic Programming to Image Processing},
  booktitle = {Proceedings of the IASTED International Conference on
		  Applied Informatics (AI'01)---Symposium Advances in
		  Computer Applications},
  year = {2001},
  address = {Innsbruck, Austria},
  month = feb,
  pages = {577--581},
  publisher = {ACTA Press},
  editor = {M.H.~Hamsa},
  abstract = { This paper presents the evolution of algorithms
		  implementation in image processing libraries and discusses
		  the limits of these implementations in terms of
		  reusability. In particular, we show that in C++, an
		  algorithm can have a general implementation; said
		  differently, an implementation can be generic, i.e.,
		  independent of both the input aggregate type and the type
		  of the data contained in the input aggregate. A total
		  reusability of algorithms can therefore be obtained;
		  moreover, a generic implementation is more natural and does
		  not introduce a meaningful additional cost in execution
		  time as compared to an implementation dedicated to a
		  particular input type. }
}
@techreport{geraud.99.tr01,
  author = {Thierry G\'eraud and Alexandre Duret-Lutz},
  title = {Composants g\'en\'eriques de calcul scientifique},
  institution = {EPITA Research and Development Laboratory},
  year = {1999},
  type = {Technical Report},
  number = {9901},
  address = {Paris},
  month = mar,
  pdf = {adl/geraud.99.tr01.pdf},
  abstract = {Dans le cadre de l'{\'e}criture en C++ d'une
		  biblioth{\`e}que de traitements d'images et d'un atelier de
		  programmation par composants d'une cha{\^i}ne de
		  traitements, nous nous sommes fix{\'e}s deux objectifs
		  principaux : rendre les traitements g{\'e}n{\'e}riques
		  vis-{\`a}-vis du type de ses entr{\'e}es sans entra{\^i}ner
		  de surco{\^u}t significatif {\`a} l'ex{\'e}cution, et
		  pouvoir ex{\'e}cuter un traitement lorsqu'il a et{\'e}
		  introduit ult{\'e}rieurement {\`a} la compilation de
		  l'atelier. \par Le premier objectif est atteint a l'aide de
		  programmation g{\'e}n{\'e}rique et de la traduction en
		  polymorphisme statique de certains idiomes (\textit{design
		  patterns}) d{\'e}finis pour le polymorphisme dynamique. La
		  probl{\'e}matique du second objectif est double. Tout
		  d'abord, nous devions r{\'e}aliser la mise en
		  correspondance d'un traitement dont les entr{\'e}es-sorties
		  sont des types abstraits et de la routine
		  g{\'e}n{\'e}rique, charg{\'e}e du traitement, dont les
		  param{\`e}tres sont des types concrets ; ensuite, nous
		  devions pouvoir compiler et lier de nouveaux traitements a
		  la vol{\'e}e, lors de l'ex{\'e}cution de l'atelier. Pour
		  atteindre ce double objectif, nous utilisons de la
		  programmation g{\'e}n{\'e}rative et nous pratiquons
		  l'instanciation paresseuse (\textit{lazy}) de code
		  g{\'e}n{\'e}rique.\par Les solutions que nous apportons
		  permettent la gestion de composants r{\'e}utilisables de
		  calcul scientifique, ce qui, {\`a} notre connaissance, est original. }
}
@inproceedings{german.07.cae,
  author = {Daniel M. German and Lloyd Burchill and Alexandre
		  Duret-Lutz and S{\'e}bastien P{\'e}rez-Duarte and Emmanuel
		  P{\'e}rez-Duarte and Josh Sommers},
  title = {Flattening the Viewable Sphere},
  booktitle = {Proceedings of the Third Eurographics Conference on
		  Computational Aesthetics in Graphics, Visualization and
		  Imaging (CAe'07)},
  year = {2007},
  location = {Alberta, Canada},
  pages = {23--28},
  numpages = {6},
  doi = {10.2312/COMPAESTH/COMPAESTH07/023-028},
  publisher = {Eurographics Association},
  note = {Artistic Submission},
  abstract = {The viewable sphere corresponds to the space that
		  surrounds us. The evolution of photography and panoramic
		  software and hardware has made it possible for anybody to
		  capture the viewable sphere. It is now up to the artist to
		  determine what can be done with this raw material. In this
		  paper we explore the underdeveloped field of flat panoramas
		  from an artistic point of view. We argue that its future
		  lies in the exploration of conformal mappings, specialized
		  software, and the interaction of its practitioners via the
		  Internet.},
  pdf = {adl/german.07.cae.pdf}
}
@inproceedings{michaud.15.spin,
  author = {Thibaud Michaud and Alexandre Duret-Lutz},
  title = {Practical Stutter-Invariance Checks for {$\omega$}-Regular
		  Languages},
  booktitle = {Proceedings of the 22th International SPIN Symposium on
		  Model Checking of Software (SPIN'15)},
  year = 2015,
  pages = {84--101},
  series = {Lecture Notes in Computer Science},
  volume = 9232,
  publisher = {Springer},
  month = aug,
  abstract = {We propose several automata-based constructions that check
		  whether a specification is stutter-invariant. These
		  constructions assume that a specification and its negation
		  can be translated into B{\"u}chi automata, but aside from
		  that, they are independent of the specification formalism.
		  These transformations were inspired by a construction due
		  to Holzmann and Kupferman, but that we broke down into two
		  operations that can have different realizations, and that
		  can be combined in different ways. As it turns out,
		  implementing only one of these operations is needed to
		  obtain a functional stutter-invariant check. Finally we
		  have implemented these techniques in a tool so that users
		  can easily check whether an LTL or PSL formula is
		  stutter-invariant.},
  pdf = {adl/michaud.15.spin.pdf},
  doi = {10.1007/978-3-319-23404-5_7}
}
@inproceedings{renault.13.lpar,
  author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title = {Three {SCC}-based Emptiness Checks for Generalized
		  {B\"u}chi Automata},
  booktitle = {Proceedings of the 19th International Conference on Logic
		  for Programming, Artificial Intelligence, and Reasoning
		  (LPAR-19)},
  editor = {Ken McMillan and Aart Middeldorp and Andrei Voronkov },
  year = {2013},
  pages = {668--682},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {8312},
  month = dec,
  abstract = { The automata-theoretic approach for the verification of
		  linear time properties involves checking the emptiness of a
		  B{\"u}chi automaton. However generalized B{\"u}chi
		  automata, with multiple acceptance sets, are preferred when
		  verifying under weak fairness hypotheses. Existing
		  emptiness checks for which the complexity is independent of
		  the number of acceptance sets are all based on the
		  enumeration of Strongly Connected Components (SCCs).

		  In this paper, we review the state of the art SCC
		  enumeration algorithms to study how they can be turned into
		  emptiness checks. This leads us to define two new emptiness
		  check algorithms (one of them based on the Union Find data
		  structure), introduce new optimizations, and show that one
		  of these can be of benefit to a classic SCCs enumeration
		  algorithm. We have implemented all these variants to
		  compare their relative performances and the overhead
		  induced by the emptiness check compared to the
		  corresponding SCCs enumeration algorithm. Our experiments
		  shows that these three algorithms are comparable.},
  pdf = {adl/renault.13.lpar.pdf},
  doi = {10.1007/978-3-642-45221-5_44}
}
@inproceedings{renault.13.tacas,
  author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title = {Strength-Based Decomposition of the Property {B\"u}chi
		  Automaton for Faster Model Checking},
  booktitle = {Proceedings of the 19th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'13)},
  editor = {Nir Piterman and Scott A. Smolka},
  year = {2013},
  month = mar,
  pages = {580--593},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7795},
  abstract = {The automata-theoretic approach for model checking of
		  linear-time temporal properties involves the emptiness
		  check of a large B{\"u}chi automaton. Specialized
		  emptiness-check algorithms have been proposed for the cases
		  where the property is represented by a weak or terminal
		  automaton.

		  When the property automaton does not fall into these
		  categories, a general emptiness check is required. This
		  paper focuses on this class of properties. We refine
		  previous approaches by classifying strongly-connected
		  components rather than automata, and suggest a
		  decomposition of the property automaton into three smaller
		  automata capturing the terminal, weak, and the remaining
		  strong behaviors of the property. The three corresponding
		  emptiness checks can be performed independently, using the
		  most appropriate algorithm.

		  Such a decomposition approach can be used with any
		  automata-based model checker. We illustrate the interest of
		  this new approach using explicit and symbolic LTL model
		  checkers.},
  pdf = {adl/renault.13.tacas.pdf},
  doi = {10.1007/978-3-642-36742-7_42}
}
@inproceedings{renault.15.tacas,
  author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title = {Parallel Explicit Model Checking for Generalized {B\"u}chi
		  Automata},
  booktitle = {Proceedings of the 19th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'15)},
  editor = {Christel Baier and Cesare Tinelli},
  year = 2015,
  month = apr,
  pages = {613--627},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 9035,
  abstract = {We present new parallel emptiness checks for LTL model
		  checking. Unlike existing parallel emptiness checks, these
		  are based on an SCC enumeration, support generalized Buchi
		  acceptance, and require no synchronization points nor
		  repair procedures. A salient feature of our algorithms is
		  the use of a global union-find data structure in which
		  multiple threads share structural information about the
		  automaton being checked. Our prototype implementation has
		  encouraging performances: the new emptiness checks have
		  better speedup than existing algorithms in half of our
		  experiments.},
  pdf = {adl/renault.15.tacas.pdf},
  doi = {10.1007/978-3-662-46681-0_56}
}
@article{renault.16.sttt,
  author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title = {Variations on Parallel Explicit Model Checking for
		  Generalized {B\"u}chi Automata},
  journal = {International Journal on Software Tools for Technology
		  Transfer (STTT)},
  year = 2017,
  note = {First published online on 26 April 2016.},
  volume = 19,
  number = 6,
  pages = {653--673},
  month = nov,
  publisher = {Springer},
  abstract = {We present new parallel explicit emptiness checks
                  for LTL model checking. Unlike existing parallel
                  emptiness checks, these are based on a Strongly
                  Connected Component (SCC) enumeration, support
                  generalized {B\"u}chi acceptance, and require no
                  synchronization points nor recomputing procedures. A
                  salient feature of our algorithms is the use of a
                  global union-find data structure in which multiple
                  threads share structural information about the
                  automaton checked. Besides these basic algorithms,
                  we present one architectural variant isolating
                  threads that write to the union-find, and one
                  extension that decomposes the automaton based on the
                  strength of its SCCs to use more optimized emptiness
                  checks. The results from an extensive
                  experimentation of our algorithms and their
                  variations show encouraging performances, especially
                  when the decomposition technique is used.},
  doi = {10.1007/s10009-016-0422-5},
  pdf = {adl/renault.16.sttt.pdf}
}
@misc{sakarovitch.12.ciaa,
  author = {Alexandre Duret-Lutz and Sylvain Lombardy and Jacques
		  Sakarovitch and Hsu-Chun Yen},
  title = {{V}aucanson 1.4.1},
  note = {Two-page flyer for the software demo session.},
  month = jul,
  year = {2012},
  howpublished = {Distributed in the CIAA'12 conference booklet, not in the
		  main proceedings},
  pdf = {adl/sakarovitch.12.ciaa.flyer.pdf}
}
@article{thierry-mieg.04.gl,
  author = {Yann Thierry-Mieg and Souheib Baarir and Alexandre
		  Duret-Lutz and Fabrice Kordon},
  title = {Nouvelles techniques de model-checking pour la
		  v{\'e}rification de syst{\`e}mes complexes},
  journal = {G{\'e}nie Logiciel},
  year = {2004},
  number = {69},
  pages = {17--23},
  month = jun,
  pdf = {adl/thierry-mieg.04.gl.pdf}
}
@inproceedings{xue.03.icip,
  author = {Heru Xue and Thierry G{\'e}raud and Alexandre Duret-Lutz},
  title = {Multi-band Segmentation using Morphological Clustering and
		  Fusion; Application to Color Image Segmentation},
  booktitle = {Proceedings of the IEEE International Conference on Image
		  Processing (ICIP 2003)},
  year = {2003},
  address = {Barcelona, Spain},
  month = sep,
  abstract = { In this paper we propose a novel approach for color image
		  segmentation. Our approach is based on segmentation of
		  subsets of bands using mathematical morphology followed by
		  the fusion of the resulting segmentation "channels". For
		  color images the band subsets are chosen as RG, RB and GB
		  pairs, whose 2D histograms are processed as projections of
		  a 3D histogram. The segmentations in 2D color spaces are
		  obtained using the watershed algorithm. These 2D
		  segmentations are then combined to obtain a final result
		  using a region split-and-merge process. The CIE $L^*a^*b^*$
		  color space is used to measure the color distance. Our
		  approach results in improved performance and can be
		  generalized for multiband segmentation of images such as
		  multi-spectral satellite images.},
  doi = {10.1109/ICIP.2003.1246971}
}
@misc{tourneur.17.misc,
  author = {Vincent Tourneur and Alexandre Duret-Lutz},
  title = {Fixes for two equations in \emph{The Blow-Up
in Translating LTL to Deterministic Automata} by Kupferman and Rosenberg},
  howpublished = {Online pdf.},
  note = {The original authors have reviewed the fixes and agreed with them.},
  month = feb,
  year = 2017,
  pdf = {adl/tourneur.17.misc.pdf}
}