Journée du 30 Mai 2008

Lieu

IBISC: comment y aller (tour Evry2, 4eme étage, salle de réunion)

Programme

14h00-15h00 : Tayssir Touili (LIAFA -Paris 7), SPADE: Verification of Multithreaded Dynamic and Recursive Programs

Abstract: We consider the problem of model-checking of multithreaded programs with recursive procedure calls, result passing between recursive procedures, dynamic creation of parallel processes, and synchronisation between parallel threads.

To represent such programs accurately, we define the model SPAD that can be seen as the extension with synchronisation of the class PAD (the subclass of the rewrite systems PRS where parallel composition is not allowed in the left-hand sides of the rules). We consider the reachability problem of this model, which is undecidable. We reduce this problem to the computation of abstractions of the sets of execution paths of the program, and we propose a generic technique that can compute different abstractions (of different precisions and different costs) of these sets.

We implemented our techniques in a tool called SPADE, and we applied this tool to different case studies. Our results are encouraging. In particular, we were able to automatically find two bugs in two versions of a Windows NT Bluetooth driver.

15h00-15h30 : Antoine Spicher, IBISC, Univ. Evry Val-d'Essone
Calcul membranaire en MGS pour l'analyse du protocole Needham-Schroeder

Abstract:Nous présenterons le cas du calcul par membranes dans le contexte de MGS, un langage de programmation dédié à la modélisation et à la simulation de systèmes dynamiques à structure dynamique. Nous développerons dans un premier temps l'approche topologique de ce langage que nous appliquerons ensuite à l'analyse du protocole Needham-Schroeder. Cette analyse met en évidence l'attaque logique connue à travers l'utilsation originale de la réécriture de membranes imbriquées qui permet d'ajuster facilement les conditions de détection d'une attaque.

15h30-16h00: pause café

16h00-16h30: vie du groupe