SAFA Workshop

October 6th and 7th, 2010

SAFA Annual Workshop on Formal Techniques (SAFA’2010)

October, 6th, 2010

13:30 - Opening of the workshop
13:40 - Invited talk
Quantifying Robustness by Symbolic Model Checking
Emmanuelle Encrenaz,
Laboratoire d'informatique de Paris VI (LIP6),
Université Pierre et Marie Curie (Paris VI)
14:30 - Session 1: Language theory
A Locally Nameless Theory of Objects
L. Henrio, F. Kammüller, B. Lutz and H. Sudhof
CNRS – I3S – INRIA, Sophia-Antipolis, Technische Universität Berlin
15:00 - Coffee break
15:30 - Session 2: Models and Properties
PSL vs. CCSL
Régis Gascon, Julien DeAntoni, Frédéric Mallet
EPI Aoste, I3S/INRIA, Sophia Antipolis, France
Model checking applied to mobile agent system
Cyril Dumont, Fabrice Mourlin
LACL, Paris 12 University
Experiments with distributed Model-Checking of group-based applications
Ludovic Henrio & Éric Madelaine
INRIA Sophia Antipolis, CNRS - I3S - Univ. Nice Sophia Antipolis
Construction of Models Needs Idempotent Transformations
Clementine Nemo, Mireille Blay-Fornarino
Université de Nice - Sophia Antipolis, Laboratoire I3S (CNRS-UNSA)
17:30 - End of first day

October, 7th, 2010

9:30 - Session 3: Security
Software Un-security Exploitation Evaluation
Christèle Faure
Safe River
A Formal Security Model for the Verification of Automotive Embedded Applications
Gabriel Pedroza, Ludovic Apvrille, Renaud Pacalet
System-on-Chip Laboratory (LabSoC), Institut Telecom, Telecom ParisTech, LTCI CNRS
10:30 - Coffee break
11:00 - Session 4: Embedded systems
Logical Time @ Work : The RT-Simex project
Julien DeAntoni, Frédéric Mallet, Charles André, Frédéric Thomas
EPI Aoste, INRIA Méditerranée & UMR CNRS I3S Obeo, Model Driven Company
Communication Refinement for SOC Design
Hocine Mokrani, Rabéa Ameur-Boulifa, Sophie Coudert, Emmanuelle Encrenaz-Tiphene
System-on-Chip Laboratory (LabSoC), GET/Telecom-Paris, Laboratoire d’informatique de Paris VI
12:00 - Closure of the workshop

Speakers :

Emmanuelle ENCRENAZ
Laboratoire d'informatique de Paris VI
Université Pierre et Marie Curie (Paris VI)
"Quantifying Robustness by Symbolic Model Checking"

Selected papers:
- A Locally Nameless Theory of Objects
- PSL vs. CCSL
- Model checking applied to mobile agent system
- Logical Time @ Work : The RT-Simex project
- Experiments with distributed Model-Checking of group-based applications
- Construction of Models Needs Idempotent Transformations
- Software Un-security Exploitation Evaluation
- Communication Refinement for SOC Design
- A Formal Security Model for the Verification of Automotive Embedded Applications