Mardi 7 Octobre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Le langage asymptotique des courbes lisses |
Description: |
Thierry Monteil Le tracé d'une courbe sur une grille produit une suite de pixels consécutifsqui peut être représentée par un mot sur l'alphabet {droite, haut, gauche,bas}. Ce codage établit un dictionnaire entre objets géométriques (oudifférentiels) et propriétés combinatoires sur les mots. Par exemple, lecodage des segments de droites correspond aux mots dits 1-équilibrés, quisont les facteurs finis des mots sturmiens.Une méthode classique pour analyser une courbe lisse discrétisée consiste àdécomposer son codage en mots 1-équilibrés maximaux, qui servent alors detangentes discrètes. Sans ajout d'hypothèses, les estimateurs de tangentesou de courbure associés ne convergent pas nécéssairement lorsque la maillede la grille tend vers zéro.Une raison possible est la suivante : certains mots non 1-équilibrés peuventapparaître dans le codage de courbes lisses pour des mailles arbitrairementfines.Let but de cet exposé est de décrire ce langage et voir ce qu'on peut luifaire dire. |
Jeudi 9 Octobre
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. |
Lundi 13 Octobre
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 todays Web, and it is this feature that we leverage and exploit in our research work at the Sapienza University of Romes 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. |
Mardi 14 Octobre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Transcendence et algorithme de remplacement |
Description: |
Gérard Duchamp |
Mardi 21 Octobre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A general theory of Wilf-equivalence for Catalan structures |
Description: |
Mathilde Bouvel It is a commonly observed phenomenon in enumerative combinatorics thatseveral combinatorial classes share the same enumeration. For any twoclasses which seem to have the same enumeration sequence, a naturalproblem is to prove that it is indeed the case, ideally with abijective proof that allows to map the structure of one class to thatof the other.Such coincidences of enumeration are called Wilf-equivalences in thecontext of pattern-avoiding permutation classes (the definition ofpattern-avoidance will be given during the talk). Wilf-equivalence hasbeen a popular topic in the research on pattern-avoiding permutations,from its beginnings in the seventies until now. It is fair to say thatmost of the works done so far are specific to given pairs ofequi-numerous classes, thus forming a sort of "case-by-case catalogue"of the known Wilf-equivalences.In this talk, we explore a different approach: we are interested indescribing all Wilf-equivalences between permutations classes definedby the avoidance of two patterns: 231 and an additional pattern p(w.l.o.g., we can assume that p itself avoids 231). We will explainthat this is one way of phrasing a seemingly more general (butactually equivalent) question: that of describing allWilf-equivalences between classes of Catalan objects subject to onefurther avoidance restriction. Such classes are denoted Av(A), A beinga Catalan object.Our results, to be presented in the talk, are the following.First, we define an equivalence relation ~ among Catalan objects. Ourmain result is that it refines Wilf-equivalence: if A ~ B, then Av(A)and Av(B) have the same enumeration. The proof is subdivided inseveral cases, and it is bijective in all cases but one. We furtherconjecture that the converse statement holds, i.e., that this relation~ coincides with Wilf-equivalence.Then, we show how to enumerate the number of equivalence classes for~, hereby providing an upper bound on the number of Wilf-equivalenceclasses.It is also interesting to study a special ~-equivalence class, whichcan be understood at a very fine level of details. Our results on this~-class (called the "main" one) unify and generalize several resultsof the literature on Wilf-equivalence.Finally, we explain how our bijective cases in the proof of the maintheorem can often be refined to provide comparison results between theenumerations of classes Av(A) and Av(B) when A and B are notequivalent for ~. A consequence is that the "main" ~-class correspondsto the largest possible enumeration sequence.This is a joint work with Michael Albert (University of Otago), and apreprint is available at arXiv:1407.8261. |
Jeudi 23 Octobre
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.) |
Vendredi 24 Octobre
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. |
Mardi 28 Octobre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Graphes d'interaction et équations d'évolution |
Description: |
Gérard Duchamp |
Jeudi 30 Octobre
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. |
Jeudi 6 Novembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Introduction to Partial Order Reductions |
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 (PORs) are a family of techniques attempting to cope with this by constructing an equivalent state space where irrelevant executions of the original are discarded.
This talk will be a gentle introduction to the topic. We will focus on Godefroid's persistent sets, prove that a selective exploration based on them visits all deadlocks, discuss the two main classes of algorithms for computing them, and finish, time permitting, with an overview of the conceptual similarities and differences between PORs and the unfolding technique. |
Mardi 18 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Cryptophie : Black-box Trace and Revoke Codes |
Description: |
Phan Duong Hiuu |
Jeudi 20 Novembre
Heure: |
15:30 - 16:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Abstraction and Modular Verification of Services Using Symbolic Observation Graph (SOG) |
Description: |
Hanene Ochi For automatically composing services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) without including any additional information that can be used to disclose the privacy of these services. The compatibility between two services can be based either on some generic properties or specific ones . This talk will present my work during my thesis about the problem considering these kinds of compatibility criteria, and we will introduce approches for the automatic abstraction of services and to the modular checking of their compatibility using their abstract models only. To abstract services, we use the symbolic observation graph (SOG) approach that preserves necessary informa tion for service composition and hides private information. We will show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of services instead of the original composite service. |
Vendredi 21 Novembre
Heure: |
10:30 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Chemins en ludique non-linéaire |
Description: |
Alice Pavaux La ludique est une théorie logique basée sur l'interaction, introduite il y a une quinzaine d'années par J.-Y. Girard. Elle s'inscrit dans un contexte marqué par les avancées importantes en théorie de la démonstration et en sémantique des langages de programmation permises par la logique linéaire. On se propose ici d'étudier les mécanismes de l'interaction dans une variante non-linéaire de la ludique, afin de poser les outils nécessaires à l'étude des types dans ce cadre. Cela se fera en décrivant les chemins suivis au cours de l'interaction au sein des desseins, les objets de la ludique. La non-linéarité permet de ne pas se restreindre au fragment multiplicatif-additif de la logique linéaire. |
Mardi 25 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Le diamètre asymptotique des associaèdres généralisés |
Description: |
Lionel Pournin Les associaèdres généralisés ont été introduits par SergeyFomin et Andrei Zelevinsky dans le cadre de la théorie des algèbresamassées, et réalisés géométriquement par Chapoton, Fomin etZelevinsky. Ils sont associés à n'importe quel groupe de Coxeter fini.Parmi eux figurent trois familles infinies de polytopes : lesassociaèdres de type A (associaèdres usuels), de type B ou C(cycloèdres), et de type D.Le diamètre asymptotique des associaèdres de types A, B (ou C), et Dest maintenant connu et cet exposé passera en revue les cas des typesB (ou C), et D. Les preuves ne seront pas données entièrement, maisseulement esquissées. Quelques questions associées seront finalementdiscutées. |
Jeudi 27 Novembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Precise Robustness Analysis of Real-Time Systems |
Description: |
Étienne André Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to characterise the system local robustness, and hence to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system. This work is a joint work with Laure Petrucci. |
Vendredi 28 Novembre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
New applications of moment-SOS hierarchies |
Description: |
Victor Magron Semidefinite programming is relevant to a wide range of mathematic fields, including combinatorial optimization, control theory, matrix completion. In 2001, Lasserre introduced a hierarchy of semidefinite relaxations for particular polynomial instances of the Generalized Moment Problem (GMP). My talk emphasizes new applications of this moment-SOS hierarchy, investigated during my PhD and Postdoc research.
In the context of formal proofs for nonlinear optimization, one can combine the moment-SOS hierarchy with maxplus approximation of semiconvex functions. Such a framework is mandatory for formal certification of nonlinear inequalities, occurring by thousands in the proof of Kepler Conjecture by Hales.
I also present how to approximate, as closely as desired, the Pareto curve associated with bicriteria polynomial optimization problems or the projections of semialgebraic sets. For each problem, one builds a hierarchy of semidefinite programs, so that the sequence of bounds converges in L1 norm.
Finally, this hierarchy allows to analyze programs containing loop invariants with polynomial assignments. |
Mardi 2 Décembre
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Robust network design with uncertain outsourcing cost |
Description: |
Michael Poss The expansion of a telecommunications network faces two sources of uncertainty, which are the demand for traffic that shall transit through the expanded network and the outsourcing cost that the network operator will have to pay to handle the traffic that exceeds the capacity of its network. The latter is determined by the future cost of telecommunications services, whose negative correlation with the total demand is empirically measured in the literature through the price elasticity of demand. Unlike previous robust optimization works on the subject, we consider in this paper both sources of uncertainty and the correlation between them. The resulting mathematical model is a linear program that exhibits a constraint with quadratic dependency on the uncertainties. To solve the model, we propose a decomposition approach that avoids considering the constraint for all scenarios. Instead, we use a cutting plane algorithm that generates required scenarios on the fly by solving linear multiplicative programs. Computational experiments realized on the networks from SNDlib show that our approach is orders of magnitude faster than the classical semidefinite programming reformulation for such problems. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Analyse en moyenne d'algorithmes sur les graphes |
Description: |
Vlady Ravelomanana |
Mardi 9 Décembre
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Complexity aspects of graph convexities |
Description: |
Mitre Dourado In the first half of the talk, I will survey the basic concepts, problems and main known results related to computational complexity aspects of graph convexities. In the second half, I will present some new results on the Radon number in the geodetic convexity, among them a polynomial time algorithm for finding the Radon number of unit interval graphs.
This is a joint work with: Jayme Luiz Szwarcfiter Alexandre Toman |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Asymptotic expansion for random tensor models |
Description: |
Adrian Tanasa Three-dimensional random tensor models are a natural generalization ofthe celebrated matrix models. The associated tensor graphs, or 3Dmaps, can be classified with respect to a particular integer orhalf-integer, the degree of the respective graph.I will present in this talk a combinatorial analysis of the generalterm of the asymptotic expansion in N, the size of the tensor, of aparticular random tensor model, the so-called multi-orientable model.I will then present some enumerative results and show which are thedominant configurations of a given degree; several examples will alsobe given. |
Jeudi 11 Décembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
CosyVerif: An Open Source Extensible Verification Environment |
Description: |
Étienne André Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of eff ective integrated formal methods. Here, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata. This work is implemented in the CosyVerif platform, a modular framework integrating verification software tools of the Paris regions. This is a joint work with the CosyVerif team. |
Vendredi 12 Décembre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Asynchronous Interaction with Theorem Provers: ProofGeneral's Last March |
Description: |
Carst Tankink This year ProofGeneral, the generic Emacs-interface for proof assistants, celebrates its 20th birthday. The tool is showing its age, however, by only allowing a user to work at a single point at the time, and having to re-evaluate an entire proof script in reaction to changes at the beginning. In this talk, I will discuss our recent efforts to changing this situation: based on a previous endeavour in Isabelle, we have adapted the Coq proof assistant to work with the jEdit text editor. This editor has no user-visible notion of "State": the entire proof is always available to the proof assistant, allowing it to react to changes in the document in a more intelligent manner: by scheduling proofs in parallel and by postponing computation that are of no direct interest to the author. I will not go into full technical details in this talk, but give a demo of the current prototype, and discuss the ramifications of such a model in the longer term. |
Mardi 16 Décembre
Heure: |
14:10 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Plus long cycle dans les graphes aléatoires |
Description: |
Vlady Ravelomanana |
Heure: |
15:10 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Dependence and phase change in random m-ary search trees |
Description: |
Hsien-Kuei Hwang |
Jeudi 18 Décembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Teaching Formal Methods: Experience at UPMC and UP13 with CosyVerif |
Description: |
Laure Petrucci Nowadays, students are more and more demanding for practical coursework, which is a challenge when teaching formal approaches to software engineering. The solution is to provide environments for such hands-on sessions and homework, but this raises numerous difficulties. The environment must be: (i) multi-platform (Mac OS, Linux, Windows) so as to enable student practice at home, (ii) easy to deploy, (iii) easy to use and to take charge of, and (iv) flexible enough to enable the integration of new notations and associated services.
CosyVerif is a software environment dedicated to graphical notations, that provides the mechanisms and means for an easy integration of additional existing software for teaching (or demonstration) purposes. This makes it an interesting platform to establish new courses.
This paper presents our experience using CosyVerif for teaching Petri nets and parametric timed automata in two universities of the Paris region, i.e. Université Pierre et Marie Curie, and Université Paris 13. We also use CosyVerif to build demonstrators of Ph.D. students' work. |
|
|