21 Novembre - 27 Novembre


Retour à la vue des calendrier
Mardi 22 Novembre
Heure: 16:15 - 19:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Double régularisation des polyzêtas en les multi-indices négatifs
Description: Quoc Hoan Ngo
Jeudi 24 Novembre
Heure: 10:00 - 11:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Vers une théorie de la réécriture probabiliste
Description: Flavien Breuvart Après une récapitulation des définitions fondamentales et enjeux
de la théorie de la réduction de termes (TRS et HORS), nous allons
nous poser la question de l'ajout de composantes probabilistes.

Nous verrons que des problématiques importantes apparaissent à un
niveau très élémentaire. En fait, elles apparaissent déjà au
niveau des ARS (graphe orientés infinis décrivant une dynamique)
qui sont extrêmement généraux et contiennent les automates dont
la généralisation probabiliste a été abondamment étudiée. En
utilisant ces travaux sur les automates, et plus généralement sur
les co-algèbres, nous avons décrit un formalisme pouvant, nous
l'espérons, traiter élégamment des problèmes de réécritures
probabilistes.
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Regular Model Checking: Vérification et systèmes de réécriture
Description: Tayssir Touili Nous nous intéressons dans cet exposé au model-checking des systèmes infinis, notamment les systèmes paramétrés et les programmes récursifs parallèles.
Nous présentons un cadre uniforme pour la vérification algorithmique de ces systèmes. Ce cadre est basé sur la représentation des ensembles de configurations par des automates de mots ou d'arbres, et la représentation des relations de transition des systèmes par des règles de réécritures de mots ou de termes. Le problème de la vérification est ensuite réduit au calcul des ensembles des accessibles dans ce cadre.
Vendredi 25 Novembre
Heure: 11:00 - 12:30
Lieu: Salle A303, bâtiment A, Université de Villetaneuse
Résumé: Implémentation de complexité implicite dans les compilateurs
Description: Thomas Rubiano La complexité implicite s’intéresse à la gestion des ressources, temps
ou espace, consommées par un programme. Comme les méthodes de
complexité implicite fonctionnent à l’aide de critères purement
syntaxiques, ces analyses peuvent être faites au moment de la
compilation du programme (et pas au cours de son exécution) et le
“certificat” obtenu peut alors être directement associé à
l’exécutable. De plus, les compilateurs manipulent dans leurs
représentations intermédiaires des langages proches de l’assembleur
avec un accès au graphe de flot de contrôle. Ainsi, on dispose
directement des outils nécessaires pour exprimer certaines méthodes de
complexité implicite. Le but initial de la thèse était d’écrire, un
plugin pour effectuer la détection de programmes qui calculent en
espace constant (Non-Size-Increasing Programs) au cours de la
compilation et en déduire automatiquement des optimisations
d’allocation de mémoire. Le premier compilateur cible a été llvm, une
passe a donc été implémentée.

Ensuite, il était prévu d’une part de continuer à implémenter des
méthodes de complexité implicite dans les compilateurs –notamment la
Size Change Termination ou les polynômes mwp qui s’expriment bien sur
un langage impératif de bas niveau. D’autre part, de chercher à
exprimer d’autres analyses dans ce genre de langage afin de comparer
de manière plus systématique les différentes analyses existantes.

C'est en apprenant les techniques utilisées dans ces deux dernières
théories que nous nous sommes intéressés à implémenter une
optimisation de pelage de boucle présentée sur un langage WHILE dans
un brouillon de Lars Kristiansen. Nous l'avons repris et baptisée:
"Calcul de degré d'invariance et composition de commandes pour du
pelage de boucle". Après avoir fait quelques tests sur le langage C à
l'aide d'un parser « jouet » en python. Une passe LLVM est en cours de
développement…

Les analyses de complexité implicites sont actuellement décrites sur
des langages « jouets ». En les portant sur des « vrais » langages de
programmation, la thèse a pour but de fournir à la communauté un outil
permettant de traiter une grande quantité d’exemples et d’avoir une
idée plus précise de l’expressivité réelle de ces analyses. De plus
elle crée un pont avec la communauté compilation afin que chacune
apporte à l'autre.

Cette thèse est financée par le projet ANR ELICA