|
|
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 sintéresse à la gestion des ressources, temps ou espace, consommées par un programme. Comme les méthodes de complexité implicite fonctionnent à laide 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é à lexécutable. De plus, les compilateurs manipulent dans leurs représentations intermédiaires des langages proches de lassembleur 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 dallocation de mémoire. Le premier compilateur cible a été llvm, une passe a donc été implémentée.
Ensuite, il était prévu dune 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 sexpriment bien sur un langage impératif de bas niveau. Dautre part, de chercher à exprimer dautres 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é dexemples et davoir une idée plus précise de lexpressivité 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 |
|
|