Bonjour,
Nous avons le plaisir de vous inviter au Séminaire des étudiants
chercheurs du LRDE. Ils présenteront le résultat de leurs travaux
le mardi 2 juillet en amphi 2 à partir de 13h.
Au programme :
- Climb :
13h00 : Antoine Hacquard "Parallélisation et Indexation de Quickref"
- Oléna :
13h30 : Thibault Buatois "Segmentation de tumeur cérébrale par réseau de neurones convolutionnel"
14h00 : Célian Gossec "Création d'un lien entre une bibliothèque de traitement d'images en C++ haute performance vers Python"
14h30 Pause
- Spot :
14h45 : Samuel Corno "Utilisation du Scatter Search pour trouver un meilleur ordre de variable dans les BDD"
15h15 : Paul Guénézan "Exploration d'espace d'états distribuée"
15h45 : Martin Huvelle "Réimplémentation des automates testeurs dans Spot"
16h15 : Antoine Martin "Comment implémenter le support des goroutines dans go2pins"
Pour plus d’informations, voir ici : https://www.lrde.epita.fr/wiki/Student_Seminar_2019-07-02
L'entrée du séminaire est libre.
--
Daniela Becker
Responsable administrative du LRDE
Bonjour à tous,
J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :
"Vers une parallélisation efficace de la résolution du problème de
satisfaisabilité"
L'exposé se déroulera en français.
Vous êtes également cordialement invité au pot qui suivra.
Date : le mercredi 3 juillet à 14h
Lieu : en salle KB604 à l'EPITA, 14-16 rue Voltaire, Le Kremlin-Bicêtre
94270
Vous trouverez également toutes les informations sur la page web
suivante :
https://www.lrde.epita.fr/wiki/Affiche-these-LLF
Le jury sera composé de :
Rapporteurs:
* Michaël KRAJECKI, Professeur à l'Université de Reims, CReSTIC
* Laurent SIMON, Professeur à l'Université de Bordeaux, LaBRI, CNRS
Examinateurs:
* Daniel LE BERRE, Professeur à l'Université d'Artois, CRIL, CNRS
* Bertrand LE CUN, Ingénieur Senior à Google Inc.
* Clémence MAGNIEN, Directeur de Recherche au CNRS, LIP6, CNRS
Encadrants:
* Souheib BAARIR, Maître de Conférence à l'Université Paris Nanterre,
LIP6, CNRS
* Fabrice KORDON, Professeur à Sorbonne Université, LIP6, CNRS
* Julien SOPENA, Maître de Conférence à Sorbonne Université, LIP6,
CNRS, INRIA
Mots clés : satisfaisabilité booléenne, parallélisation, portfolio,
diviser pour régner, échange de clauses, outil
Le résumé de la thèse est le suivant :
Les solveurs résolvants le problème de SATisfiabilité booléenne sont
utilisés avec succès dans de nombreux contextes : vérification de
programmes et de matériels, cryptographie, bio-informatique, preuve
automatique de théorème, etc. Ceci est dû à leur capacité à résoudre
d'énormes problèmes pouvant contenir des millions de variables et des
dizaines de millions de contraintes. Alors que la plupart des solveurs
SAT ont longtemps été séquentiels, l'émergence des machines multi-cœurs
a ouvert de nouvelles perspectives dans ce domaine.
Il existe de nombreux solveurs SAT parallèles différents par leurs
stratégies, langages de programmation, bibliothèques utilisées, etc. Il
est donc difficile de comparer l'efficacité de différentes stratégies
dans un cadre unifié et équitable. De plus, l'introduction de nouvelles
approches nécessite une compréhension approfondie de l'implémentation
des solveurs déjà existants.
Cette thèse présente Painless : une plateforme générique et modulaire
permettant l'implémentation de solveurs SAT parallèles efficaces pour
les machines multi-cœurs. Elle offre une implémentation des composants
de base et sa modularité permet aux utilisateurs de créer facilement
leurs solveurs parallèles basés sur de (nouvelles) stratégies.
Painless a permis de construire et tester de nombreux solveurs. Nous
avons pu imiter le comportement de trois solveurs de l'état de l'art
tout en factorisant de nombreuses parties du code. L'efficacité de
Painless a été soulignée par le fait que ces implémentations sont au
moins aussi efficaces que les originales. De plus, lors de la
participation à la compétition annuelle internationale de solveurs SAT
parallèles, l'un de nos solveurs s'est classé 3ème en 2017 et un autre
1er en 2018.
Nous avons utilisé Painless pour mener des expériences équitables avec
des solveurs de type diviser pour régner. Celles-ci nous ont permis de
mettre en lumière des compositions originales d'heuristiques plus
performantes que celles déjà présentes dans l’état de l’art.
Enfin nous avons été en mesure de créer et tester de nouvelles
stratégies exploitant la structure modulaire des formules SAT.
L'approche que nous avons proposée utilise la topologie de la formule
pour guider le solveur vers des zones plus riches en informations,
permettant ainsi l’accélération de la résolution parallèle du problème.
A bientôt,
Ludovic LE FRIOUX
Bonjour,
Nous avons le plaisir de vous inviter au Séminaire des étudiants
de la majeure double compétence recherche (RDI) composée
d'étudiants venant aussi bien du LRDE que du LSE.
Il se déroulera le 1er juillet en amphi master à partir de 13h.
Les sujets abordés sont :
13h00 : « Modeling and Identifying Troll Farm Accounts on Twitter » -
Antoine Sainson (LSE)
13h30 : « Automatic troll farm detection on Twitter » -
Hugo Linsenmaier (LSE)
14h00 : « Génération d'états artificiels dans des espaces d'états à l'aide d'estimations
de densité paramétriques et non paramétriques. » -
Thomas de Carvalho (LRDE)
14h30 : « Estimation de la fonction de niveau de bruit à l'aide de l'arbre des formes dans
des images naturelles » -
Baptiste Esteban (LRDE)
15h15 : « Génération d'images marines réalistes » -
Charles Ginane (LRDE)
15h45 : « Integrating Mathematical Morphology with Deep Convolutional Neural Networks » -
Alexandre Kirszenberg (LRDE)
16h15 : « Introduction des opérateurs morphologiques dans les réseaux de neurones convolutionels profonds » -
Younes Koudhli (LRDE)
16h45 : « An implementation of Baker’s SUBTYPEP decision procedure » -
Léo Valais (LRDE)
Pour plus d’informations, voir ici : https://www.lrde.epita.fr/wiki/Student_Seminar_2019-07-01
L'entrée du séminaire est libre.
--
Daniela Becker
Responsable administrative du LRDE