17 Novembre - 23 Novembre


Retour à la vue des calendrier
Mardi 18 Novembre
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Cryptophie : Black-box Trace and Revoke Codes
Description: Phan Duong Hiuu
Jeudi 20 Novembre
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Abstraction and Modular Verification of Services Using Symbolic Observation Graph (SOG)
Description: Hanene Ochi For automatically composing services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) without including any additional information that can be used to disclose the privacy of these services. The compatibility between two services can be based either on some generic properties or specific ones . This talk will present my work during my thesis about the problem considering these kinds of compatibility criteria, and we will introduce approches for the automatic abstraction of services and to the modular checking of their compatibility using their abstract models only. To abstract services, we use the symbolic observation graph (SOG) approach that preserves necessary informa tion for service composition and hides private information. We will show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of services instead of the original composite service.
Vendredi 21 Novembre
Heure: 10:30 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Chemins en ludique non-linéaire
Description: Alice Pavaux La ludique est une théorie logique basée sur l'interaction, introduite il y a une quinzaine d'années par J.-Y. Girard. Elle s'inscrit dans un contexte marqué par les avancées importantes en théorie de la démonstration et en sémantique des langages de programmation permises par la logique linéaire. On se propose ici d'étudier les mécanismes de l'interaction dans une variante non-linéaire de la ludique, afin de poser les outils nécessaires à l'étude des types dans ce cadre. Cela se fera en décrivant les chemins suivis au cours de l'interaction au sein des desseins, les objets de la ludique. La non-linéarité permet de ne pas se restreindre au fragment multiplicatif-additif de la logique linéaire.