SSURFRSS

Journée SSURF

08/03/2010
Intervenant(s) : E. Jaeger (ANSSI), C. Munoz (NASA), G. Dowek (LIX), M. Pouzet (LRI)
Dans le cadre de l'action ANR SSURF (Safety and Security UndeR Focal) et à l'occasion de la soutenance de thèse de Eric Jaeger, une journée d'exposés aura lieu le lundi 8 mars 2010 au LIP6 dans la salle 549 (104 av. du Pdt. Kennedy, 75016 Paris au 5eme étage). Cette journée est ouverte à toute personne intéressée.
Le programme prévisionnel est donné ci-dessous.
Bien cordialement.
Mathieu Jaume
--------------------------
9h30 : Soutenance de la thèse de Eric Jaeger (SPI-LIP6 et ANSSI) "Etude de l'apport des méthodes formelles déductives pour les développement de sécurité"
Quelles sont les apports mais aussi les limites des méthodes formelles déductives pour les développement de sécurité ? Nous identifions quelques pièges pour les développeurs ou les évaluateurs de sécurité, avant de proposer quelques recommandations pour améliorer le niveau de confiance. Cette étude passe par une formalisation du concept de raffinement et la validation d'une méthode formelle par un plongement.
Rapporteurs : Gilles Dowek (LIX), César Muñoz (NASA Langley Research Center) Examinateurs : Béatrice Bérard (MoVE-LIP6), Sylvain Boulmé (VERIMAG), Catherine Dubois (ENSIIE) - Co-encadrante, Loic Duflot (ANSSI), Thérèse Hardin (SPI-LIP6) - Encadrante, Fairouz Kamareddine (Heriot-Watt University, Edinburgh)
14h15 : César Muñoz (NASA Langley Research Center) "A Formal Library of Set Relations and Its Application to Synchronous Languages"
Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this talk, we present a formal library of set relations for the definition, verification of properties, and execution of binary set relations. The formal library consists of two parts. The first part is a set of theories written in Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The second part is a rewriting logic specification that animates in the Maude system synchronous binary relations on sets. The library is illustrated with the operational semantics of the Plan Execution Interchange Language (PLEXIL), a rich concurrent and reactive plan execution language developed by NASA to support autonomous spacecraft operations.
15h00 : Gilles Dowek (LIX) (travail avec Guillaume Burel) "Comment montrer qu'une méthode de démonstration automatique n'est pas une instance d'une autre ?"
Résumé : Un corollaire du second théorème d'incomplétude de G"odel est que la résolution modulo n'est pas un cas particulier de la résolution ordonnée.
15h45 : Marc Pouzet (LRI) "Les programmes prennent le temps"
Un exposé fait à la demande expresse des organisateurs, garanti sans symboles grecs, pour terminer la journée dans la détente ... plus de détails sur place.

Mathieu.Jaume (at) nulllip6.fr
Mentions légales
Carte du site