14 Janvier - 20 Janvier


Retour à la vue des calendrier
Mardi 15 Janvier
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.
Jeudi 17 Janvier
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.