J. Feret -- MPRI : Interprétation Abstraite.

Année 2008-2009

• Introduction.
• transparents: (portable document)
• Analyse de propriétés numériques.
• suites arithmétiques et géométriques :
• transparents: (portable document);
• papiers : lien;
• filtres numériques :
• transparents: (postcript);
• papiers : lien;
• Analyse statique de systèmes mobiles.
• transparents: (portable document);
• papiers : lien;
• thèse : lien ;
• prototypes: lien .
• Analyse statique de systènes biologiques.
• transparents: (bientôt disponible)
• papiers : lien.

Quelques sites sur la mobilité :

• Calculi for Mobile Processes
• Searchable bibliography on Calculi for Mobile Processes
• Ambient Calculi Online

Lectures conseillées :

• Présentations des modèles :
  • A Calculus for Mobile Processes (by Robin Milner, Joachim Parrow, and David Walker).
  (Part I / Part II )
  • The Polymorphic Pi-Calculus: Theory and Implementation, PhD Thesis, David N Turner.
  • The Join-Calculus: a Calculus for Distributed Mobile Programming, PhD Thesis, Cedric Fournet.
  • Mobile ambients, (A.D. Gordon and L Cardelli).
• Analyses de flots
• Resource access control in systems of mobile agents, (M. Hennessy and J. Riely).
Analyse de control flow uniforme par typage pour un pi-calcul distribué.
• Control Flow Analysis for the pi-calculus, (C. Bodei, P. Degano, F. Nielson, and H.R. Nielson).
Analyse de control flow uniforme par interpretation abstraite pour le pi-calcul.
• Validating Firewalls in Mobile Ambients, (F. Nielson, H.R. Nielson, R.R. Hansen, and J.G. Jensen).
Analyse de control flow uniforme pour les ambients.
• Secrecy and group creation, (L. Cardelli, G. Ghelli and A. Gordon).
Système de typage pour assurer le confinement des données dans les instances récursives de processus pour le pi-calcul.
• Ambient groups and mobility types, (L. Cardelli, G. Ghelli and A. Gordon).
Système de typage pour assurer le confinement des données dans les instances récursives d'agents et d'ambients.
• Analyses de formes
• A Kleene Analysis of Mobile Ambients, (F. Nielson, H.R. Nielson and M. Sagiv).
Analyse de forme de la hierarchie des ambients par Interprétation Abstraite, à la TVLA.
• Shape Analysis for Mobile Ambients, (F. Nielson and H.R. Nielson).
Analyse de forme par interpretation abstraite des ambients avec dénombrement.
• Analyses de traces
• Anytime, anywhere: Modal logics for mobile ambients.
Une logique pour spécifier des propriétés spatiales et temporelles sur les ambients.
• A Generic Type System for the Pi-Calculus, (A. Igarashi, N. Kobayashi).
Typage des termes du pi-calcul par tes termes de CCS, puis verification par model checking d'invariants comportementaux.