28 Novembre - 4 Décembre


Retour à la vue des calendrier
Lundi 28 Novembre
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Semantically enriched methods for next generation microblog message fine-grained geolocalization
Description: Laura Di Rocco Consistent user-generated data represent a valuable source for the extraction of new types of information patterns and knowledge. The multifaceted nature of user-generated data, along with its geographic component, is being exploited to better understand social dynamics and propagation of information. Social media activities can be associated with both an explicit and an implicit geographic information component. Consider, for instance, Twitter as a typical example. In this case, georeferencing information can be explicitly available as metadata, such as the user profile location and the GPS coordinates of the device from which the activity is performed. By contrast, implicit georeferencing information can be inferred, with variable degree of confidence, by the message content itself, which may contain images, names of entities with known spatial location, or by the social relationships and interactions among users.
Our focus is on inferring the tweeting location (i.e., the position of the user when the tweet was sent) rather than the user home location. Since explicit tagging is used only in a small percentage of tweets, we will use geospatial information implicit in the messages to improve the resolution of the georeferencing process. With the aim of fully exploiting the (explicit and implicit) fine-grained georeferencing information made available by social media, the project relies on semantically enhanced and refined crowdsourced geospatial data to extract fine-grained implicit geoinformation contained in tweet contents.

Short Bio:
Laura Di Rocco is a PhD Student at University of Genoa and a visiting PhD Student at Paris Descartes University (LIPADE). Her research interests are in the areas of geospatial data and text mining on social media.
Mardi 29 Novembre
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Une analyse asymptotique des polyominos digitalement convexes.
Description: Olivier Bodini Dans cet exposé, nous montrerons comment des techniques élémentaires (transformées de Mellin) en combinatoire analytique permettent d'obtenir des résultats assez surprenants sur les polyominos. En particulier, si l'on savait correctement énumérer les polyominos digitalement convexes, nous saurions si l'hypothèse de Riemann est vraie !
Jeudi 1 Décembre
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Approches pour la modélisation et vérification des systèmes temporisés en utilisant les diagrammes états-transitions et les réseaux de Petri colorés
Description: Mahdi Benmoussa (Répétition avant soutenance de thèse.)
Nous présentons dans ce travail de thèse des approches pour la spécification et la vérification des systèmes temporisés.
La première partie concerne une méthode de spécification en utilisant les diagrammes états-transitions pour modéliser un système donné en partant d'une description textuelle.
Elle comporte plusieurs étapes et utilise des observateurs d'états et des événements afin d'engendrer le diagramme états-transitions.
Un outil qui implémente les différentes étapes de la méthode de spécification pour une application semi-automatique est présenté.
La seconde partie concerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, ce qui permet d'utiliser les méthodes de vérification.
Nous prenons en considération dans cette traduction un ensemble important des éléments syntaxiques des diagrammes états-transitions, tels que la concurrence, la hiérarchie, etc.
Un outil qui implémente la traduction pour un passage automatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.
La dernière partie concerne l'intégration des contraintes temporelles dans les deux approches précédentes.
Nous définissons des annotations pour les diagrammes états-transitions dont nous fournissons la syntaxe et la sémantique.
Ces annotations seront ensuite utilisées dans la méthode de spécification et la traduction.
Le but est de proposer des annotations faciles à comprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plus utilisées.
Vendredi 2 Décembre
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Proving array-manipulating programs without arrays
Description: David Monniaux Automatically verifying safety properties of programs is hard. Many
approaches exist for verifying programs operating on Boolean and integer
values (e.g. abstract interpretation, counterexample-guided abstraction
refinement using interpolants), but transposing them to array properties has
been fraught with difficulties.
Our work addresses that issue with a powerful and flexible abstraction that
morphes concrete array cells into a finite set of abstract ones. This
abstraction is parametric both in precision and in the back-end analysis used.

One possible application would be distributed systems, where processes
are modeled using arrays indexed by the process ID.