- Annonce

Publication accepted at ICCS 2017
by Souheib Baarir 28 Mar '17

28 Mar '17

I am happy to announce that the following paper has been accepted at the 17th International Conference on Computational Science (ICCS) to be held in Zürich, Switzerland on June 12-14. Title and authors: Title : Parallel Learning Portfolio-based solvers. Tarek Menour (1,3), Souheib Baarir(1,2,3). (1) Paris Ouest Nanterre la Défense University (2) LRDE, EPITA, Kremlin-Bicêtre, France (3) LIP6 Laboratory, CNRS UMR 7606, Paris, France. Abstract: Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SATisfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration-Exploitation using Exponential weight (EXP3), that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results in comparison with the state of the art solvers.

1 0

L'air de rien 37.0
by Daniela Becker 22 Mar '17

22 Mar '17

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°37 du bulletin du LRDE. C'est un numéro spécial dédié aux parcours professionnels de plusieurs anciens élèves du LRDE depuis la promo 2001 jusqu'à celle de 2016. Vous y trouverez également des nouvelles (et nouveaux) du LRDE. Vous pouvez télécharger le bulletin en couleur à la page suivante : http://www.lrde.epita.fr/wiki/LrdeBulletin/l-air-de-rien-37 -- Daniela Becker Responsable administrative du LRDE

1 0

FiXme 4.4 is released
by Didier Verna 05 Mar '17

05 Mar '17

Hello, I'm happy to announce the release of FiXme version 4.4. What's new in this version: * Handle existing yet empty lox files properly * Don't update the lox file in final mode * Various internals and documentation improvements. Grab it directly here: http://www.lrde.epita.fr/~didier/software/latex.php#fixme or wait until it propagates through CTAN... -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[CfPart] 10th European Lisp Symposium, Apr 3-4 2017, Brussels
by Didier Verna 03 Mar '17

03 Mar '17

ELS'17 - 10th European Lisp Symposium VUB - Vrije Universiteit Brussel Belgium April 3-4, 2017 In co-location with <Programming> 2017 Sponsors: Brunner Software GmbH, Franz Inc., LispWorks Ltd. and EPITA http://www.european-lisp-symposium.org/ Recent news: - Invited speakers announced (see below) - Registration open. Don't miss the March 13 deadline for the full <Programming> conference early bird discount! The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. Keynote speakers: - Hans Hübner -- Identity in a World of Values - Bohdan B. Khomtchouk -- How the Strengths of Lisp Facilitate Building Complex and Flexible Bioinformatics Applications Important dates: - 13 Mar 2017 Early registration deadline - 03-04 Apr 2017 Symposium - 05-06 Apr 2017 <Programming> main tack Programme chair: Alberto Riva, University of Florida, USA Programme committee: Marco Antoniotti, Università Milano Bicocca, Italy Marc Battyani, FractalConcept Theo D'Hondt, Vrije Universiteit Brussel, Belgium Marc Feeley, Université de Montreal, Canada Erick Gallesio, Université de Nice Sophia-Antipolis, France Stelian Ionescu, Google Rainer Joswig, Independent Consultant, Germany António Menezes Leitão, Technical University of Lisbon, Portugal Nick Levine, RavenPack Henry Lieberman, MIT, USA Mark Tarver, Shen Programming Group Jay McCarthy, University of Massachusetts Lowell, USA Christian Queinnec, Université Pierre et Marie Curie, France François-René Rideau, Bridgewater Associates, USA Nikodemus Siivola, ZenRobotics Ltd Alessio Stalla, Università degli Studi di Genova, Italy Chris Stacy, CS Consulting Search Keywords: #els2017, ELS 2017, ELS '17, European Lisp Symposium 2017, European Lisp Symposium '17, 10th ELS, 10th European Lisp Symposium, European Lisp Conference 2017, European Lisp Conference '17 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[Seminaire-LRDE] Séminaire du LRDE le Mercredi 8 mars 2017: Nicolas Gac, Université Paris Sud, L2S (Centrale Supélec, CNRS)
by Guillaume Tochon 01 Mar '17

01 Mar '17

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 8 mars 2017 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-03-08 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 8 mars 2017 : * 11h--12h: Calcul parallèle pour problèmes inverses -- Nicolas Gac, Université Paris Sud, L2S (Centrale Supélec, CNRS) http://webpages.lss.supelec.fr/perso/nicolas.gac/francais/index.html Les algorithmes itératifs utilisés lors de la résolution de problèmes inverses portant sur des gros volumes de données requièrent une accélération significative pour être utilisés en pratique. Sur des exemples d'applications en tomographie X et en déconvolution de signaux 1D (enregistrement sur plusieurs années de données spectrales de Mars) ou 2D (flux vidéo d'une webcam), nous présenterons notre recherche de solutions permettant la parallélisation des calculs la plus efficace possible sur les processeurs de type "many cores" que sont les GPUs. Nous exposerons ainsi la triple adéquation entre l'architecture des processeurs GPUs (CUDA de Nvidia), la (re)formulation des algorithmes et la (re)structuration des données que nous avons mises en oeuvre sur différents types d'opérateurs utilisés dans les algorithmes itératifs (projecteur, rétroprojecteur, convolution nD). Par ailleurs, nous montrerons l'attention particulière qui doit être apportée au goulot d'étranglement lié au temps de transfert entre le PC et les cartes GPUs. Enfin, nous présenterons le découpage des données que nous avons effectué afin de bénéficier pleinement d'un serveur multi-GPUs et apporterons quelques éléments de réponse sur l'utilisation des GPUs couplés à Matlab et des bibliothèques déjà existantes (CUBLAS, NVPP...). -- Nicolas Gac est maître de conférences à l'université Paris Sud. Après avoir effectué sa thèse au Gipsa-lab, à Grenoble, en adéquation algorithme architecture pour la reconstruction tomographique, il poursuit ses travaux de recherche au laboratoire des Signaux et Systèmes (L2S) sur le calcul parallèle pour les problèmes inverses sur serveurs de calculs multi-GPUs ou FPGA. Les domaines applicatifs de ses travaux sont la reconstruction tomographique, la reconnaissance radar, la localisation de sources acoustiques et le traitement de données spectrales de Mars. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

Declt 2.1 "Jonathan Archer" is out.
by Didier Verna 28 Feb '17

28 Feb '17

Hello, I'm happy to announce the release of Declt 2.1 "Jonathan Archer". Declt is an automatic reference manual generator for Common Lisp libraries. New in this release: * Handle recent change in SBCL's SB-INT:INFO API. * Handle list of contacts (strings) in ASDF systems author and maintainer slots. * Some backward-incompatible changes in the keyword arguments to the DECLT function. * More hyperlinks between systems and source files. * More robust system's packages collection (no more code walking). * More robust handling of unavailable ASDF components. * More robust naming of cross-references. Grab it at the usual place: https://www.lrde.epita.fr/~didier/software/lisp/misc.php#declt -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[Seminaire-LRDE] Séminaire du LRDE le mercredi 22 février 2017: Alexandre Abraham, INRIA
by Guillaume Tochon 15 Feb '17

15 Feb '17

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 22 février 2017 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-02-22 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 22 février 2017 : * 11h--12h: Extraction de biomarqueurs des troubles autistiques à partir de l'activité cérébrale (IRMf) par apprentissage de dictionnaire parcimonieux. -- Alexandre Abraham, INRIA http://nilearn.github.io/ L'Imagerie par Résonance Magnétique fonctionnelle (IRMf) est une source prometteuse de biomarqueurs permettant le diagnostic de troubles neuropsychiatriques sur des sujets non coopératifs. L'IRMf s'étudie en établissant un atlas de régions cérébrales représentatif de l'organisation fonctionnelle, puis en étudiant la corrélation entre leurs signaux. Pour les extraire, nous proposons une approche d'apprentissage de dictionnaire multi-sujets intégrant une pénalité imposant compacité spatiale et parcimonie. Nous sélectionnons les unités de base des réseaux fonctionnels extraits à l'aide de techniques de segmentation inspirées du domaine de la vision. Nous montons à l'échelle sur de gros jeux de données en utilisant une stratégie d'optimisation stochastique. A défaut de vérité terrain, nous proposons d'évaluer les modèles générés à l'aide de métriques de stabilité et de fidélité. Nous intégrons ensuite notre méthode de définition de régions dans un pipeline entièrement automatisé, afin de réaliser une tâche de diagnostic des troubles autistiques à travers différents sites d'acquisition et sur des sous-ensembles d'homogénéité variable. Nous montrons que nos modèles ont une meilleure performance, à la fois relativement aux métriques d'évaluation mais également sur nos résultats expérimentaux. Enfin, par une analyse post-hoc des résultats, nous montrons que la définition de région est l'étape la plus importante du pipeline et que l'approche que nous proposons obtient les meilleurs résultats. Nous fournissons également des recommandations sur les méthodes les plus performantes pour les autres étapes du pipeline. -- Alexandre Abraham est un ancien de la promo CSI 2009. Il a notamment travaillé sur le watershed topologique et les espaces couleur pour le projet Olena. Après l'EPITA, il a suivi un master IAD à l'UPMC et a réalisé sa thèse à l'INRIA sur la segmentation de signaux fonctionnels cérébraux au repos sur de grandes cohortes à des fins de diagnostic. Il travaille aujourd'hui dans l'équipe de recommandation de produits chez Criteo. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

[Seminaire-LRDE] Mercredi 8 février 2017: Séminaire spécial Automates: Akim Demaille, LRDE et Charles Paperman, Université Paris Diderot
by Guillaume Tochon 03 Feb '17

03 Feb '17

Chers collègues, Un séminaire spécial sur la thématique des automates aura lieu le Mercredi 8 février 2017 (13h30--15h00), Salle L0 du LRDE (Laboratoire de Recherche et Développement de l'EPITA). Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2017-02-08 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 8 février 2017 : * 13h30 -- 14h30: Vcsn : une visite guidée -- Akim Demaille, LRDE http://vcsn.lrde.epita.fr Vcsn est une plateforme consacrée aux automates et aux expressions rationnelles. Parce qu'elle traite une large variété de natures d'automates, elle place en son coeur le concept de "contexte", qui type les automates, les expressions rationnelles, etc. La plateforme repose sur une bibliothèque C++14 "templatée" par des contextes, au dessus de laquelle la couche "dyn" qui, grâce à de l'effacement de type et de la compilation à la volée, offre à l'utilisateur le confort d'une bibliothèque traditionnelle avec la généricité et les performances d'une bibliothèque templatée. Ces bibliothèques sont ensuite exposées au travers d'outils en ligne de commande, mais aussi Python et surtout IPython, qui permettent une exploration interactive simple d'algorithmes. La bibliothèque Vcsn repose sur un ensemble d'objets --- automates, étiquettes, poids, polynômes, expressions rationnelles et développements rationnels --- sur lesquels sont fournis plus de trois cents algorithmes. Dans certains cas, Vcsn offre des fonctionalités inégalées, et certains de ces algorithmes ont des performances supérieures à celles des projets comparables. Nous ferons une présentation de l'architecture générale de Vcsn, sous la forme d'une démonstration guidée par les questions, ainsi qu'un exposé des objectifs de Vcsn 3.0. -- Akim Demaille est enseignant-chercheur à l'EPITA depuis pratiquement la création du LRDE. Il y a enseigné la logique, la théorie des langages, la construction des compilateurs, la modélisation orientée-objet et la programmation en C++. Depuis 2013, il investit son temps de recherche dans la plateforme Vcsn. Il a également contribué à divers logiciels libres, tels GNU Autoconf, GNU Automake, GNU Bison et même GNU a2ps, à un temps où ASCII et PostScript n'étaient pas l'un et l'autre obsolètes. * 14h30 -- 15h: Un outil en ligne de manipulation d'automates et de semi-groupes -- Charles Paperman, Université Paris Diderot paperman.cadilhac.name/pairs Je présenterai un outil en ligne dont l'objectif est de manipuler et tester des propriétés algébriques pour des automates. Une courte présentation de la théorie algébrique des automates sera donnée à la volée. Les seuls concepts nécessaires à la compréhension de l'exposé sont les expressions régulières, ainsi que la minimisation et la déterminisation d'automates finis. -- Charles Paperman a fini son doctorat en 2013 sous la direction de Jean-Éric Pin et Olivier Carton, au LIAFA, et travaille désormais au laboratoire de Logique Mathématique de l'Université Paris Diderot avec Arnaud Durand. Ses sujets d'étude s'articulent autour de la logique, la théorie des automates, et la complexité des circuits, avec une approche algébrique. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

Vcsn 2.5 is released!
by Akim Demaille 31 Jan '17

31 Jan '17

The Vcsners are proud to announce the release of Vcsn 2.5, aka the k-lightest release! Vcsn is a platform dedicated to the computation of, and with, finite state machines. It provides an efficient C++ library, a Python interface, and a graphical user interface on top of IPython. Noteworthy changes include: - two new implementations to compute the k-lightest paths (aka "best" paths: with the smallest weights) in tropical automata. - several new demos showing how to use the C++ library, including a translator from (French) text messages (aka SMS) into French. - a new means for the users to configure Vcsn. This adds a new prerequisite to build Vcsn: libyaml-cpp. - a much better and faster caching system of runtime generated C++ code. Users of dyn (and therefore of Python) should note an improved amortization of the compilation costs. - several portability issues reported by users were fixed. For more information, please, see the detailed news below. People who worked on this release: - Akim Demaille - Clément Démoulins - Clément Gillard - Sarasvati Moutoucomarapoulé - Sébastien Piat - Younes Khoudli For more information, please visit http://vcsn.lrde.epita.fr, in particular https://vcsn.lrde.epita.fr/Vcsn2.5. Packages of Vcsn 2.5 should appear soon on various distributions (MacPorts, Debian, ArchLinux, Docker Hub). Vcsn 2.5 is also available online, at http://vcsn-sandbox.lrde.epita.fr. ## 2017-01-23 ### Improved error messages Parse errors were improved with caret-style reports for expressions and automata in dot (Graphviz) and daut syntax. In [5]: vcsn.Q.expression('<1/2>a + <1/0>b') RuntimeError: 1.10-14: Q: null denominator <1/2>a + <1/0>b ^^^^^ while reading expression: <1/2>a + <1/0>b In [6]: vcsn.automaton(''' ...: $ -> 0 ...: 0 -> 1 <1/2>a, b ...: 1 -> $''') RuntimeError: 3.1-16: B: unexpected trailing characters: /2 while reading: 1/2 while reading: <1/2>a, b 0 -> 1 <1/2>a, b ^^^^^^^^^^^^^^^^ while reading automaton In [7]: vcsn.automaton('digraph{vcsn_context="lal, b" 0->1[label="<2>a"]}') RuntimeError: 1.35-48: B: invalid value: 2 while reading: 2 while reading: <2>a digraph{vcsn_context="lal, b" 0->1[label="<2>a"]} ^^^^^^^^^^^^^^ while reading automaton ## 2017-01-14 ### "auto" automaton file format Pass "auto" to read_automaton (in dyn, static, Python or the Tools) to let the system guess the automaton file format (daut, dot, etc.). ## 2017-01-11 ### Sms2fr New Natural Language Processing demonstration of the computations of the lightest paths. This application is a translator from SMS (i.e., text messages) to proper French. The implementation is based on _Rewriting the orthography of SMS messages_, François Yvon, In Natural Language Engineering, volume 16, 2010. The translator uses pre-trained automata and through compositions with the automaton representing the text message, generates all possible translations of the word. The best solution is then found with a shortest path algorithm. An example is given in the `Sms2fr.ipynb` notebook. ## 2017-01-01 ### A richer dyn The `vcsn::dyn` API was enriched. All the dyn types now support the usual operators: comparisons (`==`, `!=`, `<`, `<=`, `>`, `>=`), and compositions (`+`, `*`, `&`). New functions facilitate the creation of `dyn` values from strings (`make_word`, etc.). The file `tests/demos/operators.cc` shows several examples, explained in the `C++-Library.ipynb` notebook. For instance: // A simple automaton. auto a1 = make_automaton("context = lal, q\n" "$ 0 <1/2>\n" "0 1 <2>a, <6>b\n" "1 $\n", "daut"); // Its context. auto ctx = context_of(a1); // Evaluate it. assert(evaluate(a1, make_word(ctx, "a")) == make_weight(ctx, "1")); assert(evaluate(a1, make_word(ctx, "b")) == make_weight(ctx, "3")); // Concatenate to itself. auto a2 = a1 * a1; assert(evaluate(a2, make_word(ctx, "ab")) == make_weight(ctx, "3")); // Self-conjunction, aka "power 2". auto a3 = a1 & a1; assert(evaluate(a3, make_word(ctx, "b")) == make_weight(ctx, "9")); ## 2016-12-25 ### Configuration Vcsn now supports configuration files. They will be used to provide users with a means to customize Vcsn, for instance to tune the graphical rendering of the automata, to tailor the display of expressions, etc. For a start, it provides a simple means to get the configuration information, including from Vcsn Tools. $ vcsn ipython --no-banner In [1]: import vcsn In [2]: vcsn.config('configuration.cxxflags') Out[2]: '-Qunused-arguments -O3 -g -std=c++1z' $ vcsn configuration configuration.cxxflags -Qunused-arguments -O3 -g -std=c++1z This adds a new dependency: libyaml-cpp. Beware that version 0.5.2 is buggy and will not work properly. Use 0.5.1, or 0.5.3 or more recent. ## 2016-12-20 ### compare: new algorithm Three-way comparison is now available in all the layers, as `compare`, for automata, expressions, labels, polynomials and weights. This is used in Python to implement the comparisons (`<`, `<=`, `>`, `=>`, `==`, `!=`) of expressions, and of automata (`<`, `<=`, `>`, `=>`). However, since the comparison on automata is performed on the _list_ of transitions, automata that are "very much alike" (i.e., different only by superficial details) will be considered different, so `==` and `!=` are still using a safer, but much slower, comparison. In [2]: exp = vcsn.Q.expression In [3]: exp('a').compare(exp('b')) Out[3]: -1 In [4]: exp('a').compare(exp('a')) Out[4]: 0 In [5]: exp('<3>a').compare(exp('a')) Out[5]: 1 ## 2016-12-12 ### k shortest paths algorithms Two algorithms for searching k shortest paths in graphs have been implemented: "Eppstein" and "Yen". Hence, we can now search for the k lightest (smallest with respect to weights, aka "best" paths) paths in an automaton through the "lightest" algorithm. "lightest" used to compute these paths with an inefficient heap-based implementation: aut.lightest(5) aut.lightest(5, "auto") Note that "auto" does not use the latter algorithm when returning only one path, as simpler shortest path algorithms would apply to the situation and be more efficient. It then uses Dijkstra's algorithm. It can now be called with the given Yen and Eppstein algorithms as follows: aut.lightest(5, "eppstein") aut.lightest(5, "yen") Yen's algorithm requires the given automaton to have no cycles, while Eppstein supports any type of automaton. For small values of k, Yen's algorithm has better performances than Eppstein, but with increasing values of k, Eppstein is always more efficient.

1 0

HdR Duret-Lutz, vendredi 10 février, 14h15 @ Epita
by Alexandre Duret-Lutz 30 Jan '17

30 Jan '17

Bonjour, J'ai le plaisir de vous inviter à ma soutenance d'habilitation à diriger les recherches, intitulée ``Contributions to LTL and ω-automata for Model Checking'' La soutenance aura lieu le vendredi 10 février à 14h15 à l'Epita dans l'amphi 4 (24 rue Pasteur, 94270 Le Kremlin-Bicêtre). Un plan d'accès est disponible ici: https://www.lrde.epita.fr/~adl/dl/lrde-amphi4.pdf Vous êtes également invités au pot qui suivra, dans la salle alpha du LRDE (2e étage du bâtiment X, 18 rue Pasteur). Le jury sera composé de: Javier Esparza, Tech. Univ. München, Germany, rapporteur Radu Mateescu, Inria Grenoble, France, rapporteur Moshe Y. Vardi, Rice Univ., Houston, Texas, USA, rapporteur Rüdiger Ehlers, Univ. Bremen, Germany, examinateur Stephan Merz, Inria Nancy & Loria, France, examinateur Jaco van de Pol, Univ. Twente, Netherlands, examinateur Fabrice Kordon, Univ. P.&M. Curie, Paris, France, examinateur Une version non-définitive du mémoire peut être téléchargée ici: https://www.lrde.epita.fr/~adl/dl/adl/duret.17.hdr.pdf La soutenance aura lieu en anglais, avec le résumé qui suit. We present multiple practical contributions to the automata-theoretic approach to LTL model checking. Most of these contributions are implemented in Spot (https://spot.lrde.epita.fr/) a library and a set of tools exporting reusable algorithms, with a growing user base. In particular, we will present an overview of the techniques used in our LTL-to-Büchi translator, that is now one of the leading tools available for this task. We will also discuss how we built algorithms that support automata with arbitrary acceptance conditions, and how some of these algorithms became more elegant as a consequence. Finally we will show how the set of tools that we have built can be used to improve existing algorithms by finding bugs or detecting nonoptimal results (e.g., by using a SAT-solver to find minimal deterministic omega-automata of arbitrary acceptance conditions). -- Alexandre Duret-Lutz

1 0