Annonce June 2017

annonce@lrde.epita.fr

2 participants
4 discussions

by Daniela Becker

Bonjour, nous avons le plaisir de vous annoncer la sortie du n°38 du bulletin du LRDE. C'est un numéro spécial dédié aux séminaires des étudiants-chercheurs du LRDE qui auront lieu le mardi 4 juillet 2017. Vous y trouverez le programme de la journée avec les résumés des exposés. Nous y laissons également la parole à trois de nos collègues qui ont décidé de partir pour de nouveaux horizons. Vous pouvez télécharger le bulletin en couleur à la page suivante : http://www.lrde.epita.fr/wiki/LrdeBulletin/l-air-de-rien-38 -- Daniela Becker Responsable administrative du LRDE

7 years, 5 months

Publication accepted at SAT'2017

by Souheib Baarir

I am happy to announce that the following paper has been accepted at the 20th International Conference on Theory and Applications of Satisfiability Testing to be held in Melbourne, Australia from August 28th to September 1st. "PaInleSS: a Framework for Parallel SAT Solving" Ludovic Le Frioux (1,2), Souheib Baarir (1,2,3), Julien Sopena (2), and Fabrice Kordon (2) (1) LRDE, EPITA, Kremlin-Bicêtre, France (2) Sorbonne Universites, UPMC Univ Paris 06, UMR 7606, LIP6, Paris, France CNRS, UMR 7606, LIP6, Paris, France (3) Universite Paris Nanterre, France. Abstract : Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programming, involved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool. We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers. Souheib Baarir.

7 years, 5 months

[Séminaire des étudiants CSI] Mardi 4 juillet 2017 - Salle L0

by Daniela Becker

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mardi 4 juillet 2017 à partir de 10h00 en L0 au LRDE (KB). -------------------------------------------- Au programme : SPOT — BIBLIOTHÈQUE DE MODEL CHECKING 10h00 : Un ensemble d’outils de conversion en automate de co-Büchi – ALEXANDRE GBAGUIDI AÏSSE Spot supporte des conditions d’acceptation arbitraires et propose déjà quelques conversions entre elles. Nous rajoutons de nouveaux algorithmes de conversion capables de convertir (quand c’est possible) n’importe quel automate avec une condition d’acceptation classique vers du co-Büchi déterministe. Nous présenterons ces algorithmes mis au point par Boker et Kupferman en explicitant les améliorations apportées durant leur implémentation. 10h30 : Test de vacuité bi-bande dans Spot – CLÉMENT GILLARD Lorsqu’on fait de la vérification de modèle à l’aide d’ω- automates, une opération typique est le calcul de L(AxB) ≠ Ø. Son implémentation par empty(product(A,B)) pose problème, car le produit utilise autant d’ensembles d’acception qu’il y en a dans A et dans B et ce nombre d’ensembles ne peut excéder 32 dans Spot. On propose empty(A,B) qui ne construit pas d’automate et retire cette contrainte sur les automates en entrée. 11h00 : Réduction par simulation à n pas – LAURENT XU En vérification formelle à l’aide d’ω-automates, il est utile de réduire la taille des automates. L. Clemente et R. Mayr présentent une méthode de réduction par simulation à n pas ne fonctionnant que pour les automates de Büchi et montrent que l’augmentation de ce nombre de pas améliore la réduction. Nous étudions une généralisation de la réduction d’ω- automates par simulation reposant sur la signature des états à un pas de Spot afin qu’elle fonctionne également à n pas. 11h30 : Réduction d’ordre partiel dans SPOT – VINCENT TOURNEUR Les outils de vérification formelle souffrent actuellement d’un problème de passage à l’échelle. La réduction d’ordre partiel (POR) est une des techniques permettant de la réduire notablement, en ne calculant que les données requises à la volée. Nous allons parler de l’implémentation de certains de ces algorithmes de POR dans la bibliothèque Spot, puis de leur optimisation. 13h30 : Intégration de TChecker dans Spot – ARTHUR REMAUD Les automates temporisés sont un type d'ω-automate représentant des modèles comportant des conditions de temps continu. Spot ne gère actuellement pas ce type d’automates. TChecker est un outil développé par le LaBRI travaillant sur des automates temporisés. Plutôt que réimplémenter tous les algorithmes, TChecker a été intégré dans Spot via un nouvel exécutable. 14h00 : Synthèse LTL avec Spot – THIBAUD MICHAUD Nous présentons un nouvel outil de synthèse de circuit à partir de spécifications LTL. Il réduit le problème de synthèse à un jeu à parité, qui est résolu grâce à l’un des deux algorithmes implémentés. Finalement, la stratégie gagnante est traduite en un circuit Et-Inverseur qui modélise la formule LTL d’origine. OLENA — TRAITEMENT D’IMAGES GÉNÉ- RIQUE ET PERFORMANT 14h45 : L’Arbre de partition binaire pour le traitement d’images – FABIEN HOUANG L’arbre de partition binaire est, en traitement d’images, une structure qui permet la segmentation et la recherche efficace d’information dans une image. Il peut être créé à partir de différents modèles de région et fonctions de calcul de distance entre ces régions. La construction de cet arbre se fait habituellement à partir d’une image pré-segmentée pour des questions de performance. La sensibilité de l’arbre au bruit dans l’image peut aussi être étudiée, pour trouver par exemple quels niveaux de l’arbre sont influencés par ce dernier. 15h15 : Calcul du Complexe de Morse- Smale à l’aide de coupe de ligne de partage des eaux – VICTOR COLLETTE Le complexe de Morse-Smale est un outil utile pour analyser la topologie d’une image. Son calcul étant onéreux avec un algorithme classique, L. Comic a émis l’hypothèse que son calcul pouvait être réalisé à l’aide d’un algorithme de coupe de ligne de partage des eaux. Nous parlerons donc de cette possibilité et des différents problèmes que cette solution engendre. 15h45 : Méthode d’évaluation d’évaluateur d’algorithme de détection de texte – ALIONA DANGLA Plusieurs méthodes d’évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents. Afin d’évaluer ces méthodes, la solution proposée est de confronter les évaluations automatiques avec l’évaluation humaine en considérant celle-ci comme référence. Pour l’obtenir, un site internet à été réalisé afin d’obtenir un classement cohérent. -- Daniela Becker Responsable administrative du LRDE

7 years, 6 months

Olivier Ricou participe à PyParis 2017

by Daniela Becker

Bonjour, nous avons le plaisir de vous annoncer qu'Olivier Ricou, directeur du LRDE, est invité à participer dans le cadre de la Conférence PyParis 2017 (http://www.pyparis.org) à une table ronde le mardi 13 juin 2017. Il y fera un retour d’expérience sur la création d'un MOOC Python pour les scientifiques. -- Daniela Becker Responsable administrative - LRDE

7 years, 6 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce June 2017