Octobre 2014

Heure:	16:00 - 17:00
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Unfolding-based Reachability Checking of Petri Nets
Description:	César Rodríguez In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions attempt to address this by constructing an equivalent state space where irrelevant executions of the original are discarded. A comparatively less well-known approach emerges from the use of partial-order semantics, where the state space is instead represented by a partial order where concurrent actions are simply left unordered. Petri net unfoldings are arguably the most prominent verification technique issued from this idea. In this talk, three different semantics for Petri nets will be presented, the last one of which will be the aforementioned unfolding semantics. We will then see how unfoldings can be employed in practical verification and, time permitting, how to improve the method to address additional sources of SSE.

Heure:	14:00 - 15:00
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	(Digital) goodies from the ERC Wishing Well: BabelNet, Babelfy, video games with a purpose and the Wikipedia bitaxonomy
Description:	Roberto Navigli Multilinguality is a key feature of today’s Web, and it is this feature that we leverage and exploit in our research work at the Sapienza University of Rome’s Linguistic Computing Laboratory, which I am going to overview and showcase in this talk. I will start by presenting BabelNet 2.5 (http://babelnet.org), a very large multilingual encyclopedic dictionary and semantic network, which covers 50 languages and provides both lexicographic and encyclopedic knowledge for all the open-class parts of speech, thanks to the seamless integration of WordNet, Wikipedia, Wiktionary, OmegaWiki, Wikidata and the Open Multilingual WordNet. Next, I will present Babelfy (http://babelfy.org), a unified approach that leverages BabelNet to perform word sense disambiguation and entity linking in arbitrary languages, with performance on both tasks on a par with, or surpassing, those of task-specific state-of-the-art supervised systems. In the third part of the talk I will present two approaches to large-scale knowledge acquisition and validation: video games with a purpose, a novel, powerful paradigm for the large scale acquisition and validation of knowledge and data, and WiBi (http://wibitaxonomy.org), our approach to the construction of a Wikipedia bitaxonomy, that is, the largest and most accurate currently available taxonomy of Wikipedia pages and a taxonomy of categories, aligned to each other. Bio: Roberto Navigli is an Associate Professor in the Department of Computer Science of the Sapienza University of Rome. He was awarded the Marco Cadoli 2007 AI*IA Prize for the best doctoral thesis in Artificial Intelligence and the Marco Somalvico 2013 AI*IA Prize for the best young researcher in AI. He is the recipient of an ERC Starting Grant in computer science and informatics on multilingual word sense disambiguation (2011-2016) and a co-PI of a Google Focused Research Award on Natural Language Understanding. His research lies in the field of Natural Language Processing (including word sense disambiguation and induction, ontology learning from scratch, large-scale knowledge acquisition, open information extraction and relation extraction). He has served as an area chair of ACL, WWW, and *SEM, and a senior program committee member of IJCAI. Currently he is an Associate Editor of the Artificial Intelligence Journal, a member of the editorial board of the Journal of Natural Language Engineering, a guest editor of the Journal of Web Semantics, and a former editorial board member of Computational Linguistics.

Heure:	15:30 - 16:30
Lieu:	Salle A303
Résumé:	The implementation of GPGPU for Model Checking Problems
Description:	WU Zhimin In this presentation, I will introduce the implementation of GPGPU techniques in model checking area. I target Nvidia GPU so firstly, the latest CUDA Compute Architecture will be introduced, together with the key points of GPU Program optimization. Then I will refer to some existing research on GPU accelerated Model Checking Problems. Finally, I will briefly introduce my research work. (This will be an informal presentation.)

Heure:	10:30 - 12:30
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Construction de l'exponentielle libre en logique linéaire
Description:	Luc Pellissier Groupe de travail sur une extension des méthodes introduites par Paul-André Melliès et Nicolas Tabareau pour calculer le comonoïde commutatif libre dans une catégorie avec produits (c.-à-d. un modèle de la logique linéaire multiplicative additive). On introduira les concepts nécessaires (PROPs, extensions de Kan, fins, etc.) et on expliquera sous quelles conditions on peut donner une formule close pour le calcul du comonoïde commutatif libre. On verra que ces conditions sont vérifiées dans tous les modèles connus de la logique linéaire, alors que les conditions originalement proposées par Melliès et Tabareau ne sont pas vérifiées par le modèle des espaces de finitude.

Heure:	15:30 - 16:30
Lieu:	Salle B107, bâtiment B, Université de Villetaneuse
Résumé:	Modèles et paradigmes de programmation parallèle distribuée
Description:	Camille Coti Dans cette présentation, qui sera plus un panorama qu'un séminaire de recherche, je présenterai quelques grands paradigmes de programmation parallèle distribuée à travers les modèles de mémoire distribuée et de communications inter-processus. Le but de mon exposé sera de présenter comment le caractère distribué des données est représenté et manipulé dans ces paradigmes de programmation afin de réfléchir à quelles techniques de programmation adopter selon les patterns d'accès aux données d'un programme séquentiel que l'on souhaite paralléliser. Je mettrai l'accent sur la mémoire distribuée, la mémoire partagée distribuée, les sacs de tâches, les communications implicites unilatérales et bilatérales, la parallélisation automatique par compilation.