Janvier 2019

Heure:	10:30 - 12:00
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Linear Implicative Algebras, a Brouwer-Heyting-Kolmogorov interpretation of linear logic
Description:	Luc Pellissier Implicative Algebras were recently introduced by Alexandre Miquel as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly. In this ongoing work, we show how linear logic fits in this picture: we present a notion of model of intuitionnistic linear logic in which sits both syntactic models and a localized phase semantics ; and show how to transform such a model into an algebra allowing to interpret faithfully all the connectives of classical linear logic.

Heure:	12:15 - 13:30
Lieu:	Salle A303, bâtiment A, Université de Villetaneuse
Résumé:	Towards parallel verification of concurrent systems
Description:	Hiba OUNI An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). The SOG is defined as a condensed representation of the state space based on a symbolic encoding of the nodes (sets of states). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to linear time properties. Aiming to go further in the process of tackling the state space explosion problem, we propose to parallelize the construction of the SOG using three different approaches. A multi-threaded approach based on a dynamic load balancing and a shared memory architecture, a distributed approach based on a distributed memory architecture and a hybrid (shared-distributed memory) approach that combines the two previous app roaches. We implement these algorithms, we study their performances and we compare them to each other and to the sequential construction of the SOG. Experiments show that parallel approaches can improve drastically the performances of the SOG computation regarding a sequential construction. Afterwards, we go a step forward in improving the SOG construction process by reducing, on the fly, the size of the graph. We provide a symbolic (LDD-based) dichotomy-based algorithm to canonically reduce the size of the SOG aggregates. We implement this algorithm within the three parallel approaches. We conduct experiments in order to measure the impact of the canonization on the SOG construction. Results show that the canonization allows to efficiently decrease memory consumption in all approaches. Also, it allows to improve the scalability for both distributed and hybrid approaches.

Heure:	12:15 - 13:30
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Characterizing community detection algorithms and detected modules in large-scale complex networks
Description:	Vinh Loc DAO La détection de communauté est une technique qui décompose des graphes en sous-graphes densément connectés, ce qui est particulièrement utile dans le cas de (très) grands réseaux complexes dont la visualisation est difficile. De très nombreuses méthodes, très variées ont été proposées ces dernières années. Dans un contexte où aucun consensus n'émerge autour de la notion même de communauté, ces méthodes provoquent de multiples discussions scientifiques autour de la qualité de leur résultat. Dans cette thèse, nous proposons plusieurs types d'évaluation comparative et approfondie de 16 méthodes bien connues de l'état de l'art ainsi que la caractérisation exhaustive des structures communautaires découvertes dans des réseaux réels variés provenant de domaines différents. Nos résultats - méthodes et analyses - constituent un début de boîte à outils pour l'analyste bien en peine de choisir la méthode adaptée à son étude.

Heure:	12:15 - 13:30
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Approches génériques pour le traitement des données textuelles et numériques volumineuses, changeantes et multi-vues et des données en graphes
Description:	Jean-Charles Lamirel Face à la croissance continue des informations numériques, de multiples natures, qui sont disponibles en ligne, un des challenges importants pour les linguistes et les analystes de l'information, afin de pouvoir formuler des hypothèses et de valider des modèles, est d'exploiter des outils efficaces pour l'analyse de données, capables de s'adapter à des volumes importants de données hétérogènes, changeantes et souvent et de nature distribuée et multi-vues. Nous aborderons dans cette présentation les principes généraux de la maximisation des traits, une nouvelle approche statistique générique initialement dédiée au traitement des données textuelles volumineuses, mais généralisable à tout type de données numériques dynamiques et multi-vues ou à des données hybrides (textuelles-numériques) et à des données en graphe. Nous reviendrons sur ses différentes applications à succès dans les deux cadres, supervisé et non supervisé, en comparant ses performances avec celles des méthodes de l’état de l’art sur des corpus de données de référence. Nous montrerons les avantages supplémentaires liés à son intégration dans un paradigme d’analyse multi-vues basé sur le raisonnement bayésien non supervisé. Nous mettrons finalement en évidence l’intérêt de cette méthode pour l’extraction d’information dans les grands graphes et pour la comparaison de graphes de taille et de densité variable.