Groupe de Recherche Applications Réparties
grar

L’objectif de cette UE est de présenter les techniques de base pour la recherche (étude bibliographique, présentations scientifique, rédaction d’états de l’art). Ces activités seront centrés dans le domaine des applications réparties (modélisation, vérification, réalisation).

Les thèmes abordés varient suivant les années.

Le tableau ci après indique le planning des enseignements qui seront dispensés.

Semaine
Séance Lieu
1
(30/01/2014)
Fabrice Kordon : Vérification d’un protocole de quasi-certification dans un DHT Bât 31/205
13h45-15h45
Stefan Haar : What occurrence nets reveal Bât 31/205
16h00-18h00
2
(06/02/2014)
Mathieu Jaume : contrôle d’accès versus contrôle de flots Bât 31/205
13h45-15h00
John Mullins : méthodes formelles et sécurité Bât 31/205
15h15-17h15
3
(13/02/2014)
Exposés :
  • Article 8 : présentateur : Baudry Raphael - rapporteur : Pitton Olivier
  • Article 5 : présentateur : El Rhandouri Mohammed - rapporteur : Julien Christophe
  • Article 6 : présentateur : Mangean Armel - rapporteur : Carver Damien
  • Article 7 : présentateur : Poudroux Joel - rapporteur : Bellacico Denis
  • Article 9 : présentateur : Voron Gauthier - rapporteur : Pignolet Romain
Bât 31/205
14h00-18h00
4
(20/02/2014)
Soheib Baarir Problèmes SAT et Model-checking Bât 31/205
13h45-15h45
Exposés :
  • Article 3 : présentateur : Romain Pignolet - rapporteur : El Rhandouri Mohammed
  • Article 4 : présentateur : Bellacico Denis - rapporteur : Coriat Florent
  • Article 1 : présentateur : Xu Jia Hua - rapporteur : Boumis Gorgios
16h00-18h00
5
(27/02/2014)
Nathalie Sznajder : Jeux, Vérification et Synthèse Bât 31/205
13h45-15h45
Exposés :
  • Article 11 : présentateur : Carver Damien - rapporteur : Mangean Armel
  • Article 10 : présentateur : Coriat Florent - rapporteur : Voron Gauthier
  • Article 15 : présentateur : Boumis Gorgios - rapporteur : Xu Jia Hua
16h00-18h00
6
(06/03/2014)
Béatrice Bérard : modèles temporisés Bât 31/205
13h45-15h45
Exposés :
  • Article 2 : présentateur : Benallal Mohammed - rapporteur : Leclerc Marc-Henri
  • Article 12 : présentateur : Metin Hakan - rapporteur : Poudroux Joel
  • Article 14 : présentateur : Pitton Olivier - rapporteur : Jbari Brahim
16h00-18h00
7 (jeudi 13/03/12)
Yann Thierry-Mieg : model checking symbolique Bât 31/205
13h45-15h45
Exposés :
  • Article 13 : présentateur : Leclerc Marc-Henri - rapporteur : Metin Hakan
  • Article 16 : présentateur : Jbari Brahim - rapporteur : Benallal Mohammed
  • Article 17 : présentateur : Julien Christophe - rapporteur : Baudry Raphael
16h00-18h00

Les articles à présenter

L’UE GRAR prévoit des plages dédiées à des exposés effectués par lesétudiants. L’objet de cette section est de décrire les modalités de fonctionnement de ces séances.

Les articles sont présentés par un étudiant (pas en binôme donc ;-).

Pour la présentation des articles, il vous est accordé 20 minutes + 20 minutes de questions. Les objectifs de l’exposé sont les suivants :

Les étudiants ne présentant pas le papier doivent le lire et identifier quelques questions à poser à l’intervenant. Les étudiants assistant aux exposés pourront être amenés à poser des questions au même titre que les enseignants.

Pour chaque papier présenté, l'étudiant qui a fait la présentation devra défendre les résultats (par exemple, en montrant qu'ils étendent d'autres résultats existant, donc en cherchant ses arguments dans la bibliographie du domaine). Un autre étudiant sera chargé de "s'opposer" au travail présenté (lui aussi en regardant la bibliographie du domaine). Ainsi, l'opposant devra jouer un rôle central dans la séance de questions (aidé en cela par les enseignants). Ce sera le premier à qui la parole sera donnée à l'issue de l'exposé.

Il vous est demandé de respecter le timing demandé. A titre indicatif, sachez que la note d’exposé considèrera 4 critères :

  1. compréhension de l’article et restitution, recul par rapport aux informations présentées
  2. réponses aux questions
  3. présentation orale (respect du timing, aisance, ...)
  4. qualité des transparents (pertinence du contenu principalement)

ATTENTION : le respect de ces contraintes est très important et vos exposés seront interrompus au bout de 20 minutes exactement comme cela se fait dans certaines conférences.

Vous devez choisir un article à présenter avant le 29 janvier 2014.

Pour ce faire, vous devez envoyer un mail à F. Kordon VIA CE LIEN en précisant le numéro de l’article que vous avez choisi. En cas de conflit, une stratégie de type FIFO sera adoptée ;-).

Les affectations et les dates de présentation seront mises à jour sur cette page.

Les articles

Les articles seront présentés lors des séances prévues à cet effet dans le planning. Les dates précises seront mises à jour au fur et à mesure des informations contenues dans cette page.

Les articles

Voici la liste des articles proposés par vos enseignants pour GRAR :

  1. On the Foundations of Quantitative Information Flow (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  2. IP Covert Timing Channels : Design and Detection (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  3. An Improvement of McMillan’s Unfolding Algorithm (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  4. Fairness and partial order semantics (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  5. Engineering Automotive Software (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  6. Compositional Analysis of Discrete Time Petri nets (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  7. Adaptable Intrusion Detection Systems Dedicated to Concurrent Programs : a Petri Net-Based Approach (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  8. Extending PNML Scope : a Framework to Combine Petri Nets Types (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  9. Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  10. Supervisory Control for Opacity (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  11. Modelling Opacity Using Petri Nets (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  12. Asynchronous Multi-Core Incremental SAT Solving (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  13. Guard-based Partial-Order Reduction (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  14. A Fully Verified Executable LTL Model Checker (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  15. Event-Clock Automata : A Determinizable Class of Timed Automata (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  16. Checking App Behavior Against App Descriptions (présentateur : ETUDIANT - rapporteur : ETUDIANT),
  17. Automatically Securing Permission-Based Software by Reducing the Attack Surface : An Application to Android (présentateur : ETUDIANT - rapporteur : ETUDIANT),

Certains de ces articles sont issus de revues ; ils sont en général plus longs. D’autres, plus courts, sont issus de conférences internationales. Dans tous les cas, un travail de recherche autour de la problématique introduite par le papier sera demandée (étude de références voisines) afin de replacer les travaux dans le contexte du domaine considéré.