Décembre 2016


Retour à la vue des calendrier
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.
Mardi 6 Décembre
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Streaming and communication complexity of Hamming distance
Description: Tatiana Starikovskaya
Vendredi 9 Décembre
Heure: 14:30 - 17:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Développement asymptotique des sommes harmoniques (soutenance de thèse)
Description: Van Chiên Bui En abordant les nombres spéciaux comme les sommes harmoniques ou les polyzêtas sous leur aspect combinatoire, nous introduisons d'abord la définition d'un produit entre mots, dit produit de quasi-mélange q-déformé, une généralisation des produits de mélange et de quasi-mélange, ce qui nous permet de construire des structures complètes d'algèbre de Hopf en dualité. En même temps, nous construisons des bases en dualité, contenant des bases de transcendance associées aux mots de Lyndon, et des formules explicites sur lesquelles les sommes harmoniques, les polyzêtas ou les polylogarithmes sontindexés et représentés par la factorisation de la série génératrice noncommutative diagonale. De cette façon, en identifiant les coordonnées locales, nous trouvons des relations polynomiales homogènes, en poids, entre les polyzêtas indexés par ces bases.Enfin, nous déterminons les développements asymptotiques des sommes harmoniques, indexées aussi par ces bases, grâce à leur série génératrice et à la formule d'Euler Maclaurin.Pour accompagner cette étude théorique, nous proposons des algorithmes et un package en Maple afin de calculer des bases,la structure des polyzêtas et des développements asymptotiques des sommes harmoniques.Le jury sera composé de Gérard Duchamp, Hoang Ngoc Minh,(co-directeurs), Jacky Cressson, Loïc Foissy,(rapporteurs), Sylvie Paycha, Joris van der Hoeven, Daniel Barsky, Christophe Tollu (examinateurs).
Heure: 16:00 - 19:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Double regularization of polyzetas at negative multi-indices and rational extensions (soutenance de thèse)
Description: Quoc Hoan Ngo In this PhD thesis are studied the polylogarithms and the harmonic sums at non-positive (i.e., weakly negative) multi-indices. General results about these objects in relation with Hopf algebras are pr ovided. The technics exploited here are based on thecombinatorics of noncommmutative generating series relative to the Hopf phi-huffle algebra. Our work will also propose a global process to renormalize divergent polyzetas. Finally, we will apply these ideas to non-linear dynamical systems with singular inputs.The jury will be composed of:Gérard Duchamp, Hoang Ngoc Minh (directeurs),Sylvie Paycha, Dominique Manchon (rapporteurs), Karol Penson, Vincent Rivasseau, Loic Foissy, Christophe Tollu.