Programme

La conférence aura lieu à l'ENSEIRB, conjointement aux journées du GDR GPL.

Les exposés de papiers longs durent 30 min, les autres exposés seront limités à 20 min.

 

Les actes de la conférence sont accessibles en suivant ce lien.

 

Mardi 9 Juin - Journée AFADL

9h-10h30 : Session 1 - Ouverture et articles


Accueil et présentation des journées

Pascale Le Gall, Frédéric Dadeau

Vérification parallélisée de propriétés temporelles sur des traces d'exécution, par analyse dynamique formelle (papier long)
Antoine Ferlin, Philippe Bon, Virginie Wiels and Simon Collart-Dutilleul

Une argumentation pour des exigences temps réel (papier long)
Thomas Polacsek, Virginie Wiels and Frédéric Boniol

Vers un outil de vérification formelle légère pour OCaml (papier court)
Thomas Genet, Barbara Kordy and Amaury Vansyngel

10h30-11h : Pause café
11h-12h30 : Conférence invitée (commune avec CIEL) : Bertrand Meyer
13h-14h : Déjeuner
14h-15h30 : Session 2 - Papier court, présentation de projets et travaux en cours

La composition de services dans le monde asynchrone -- Formalisation et vérification en TLA+ (papier court)
Florent Chevrou, Aurélie Hurault, Philippe Mauran, Meriem Ouederni, Philippe Quéinnec and Xavier Thirioux

Rétro ingénierie des modèles pour l'étude des Smart Grids dans le cadre du projet SESAM Grids
Gabriel Pedroza

Projet MBT_Sec – Model-Based Testing for Security Components
Elizabeta Fourneret

Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov
Olivier Hermant and Vivien Maisonneuve

15h30-16h : Pause café
16h-17h30 : Session 3 - Travaux en cours/discussions


Proving soundness of a procedure for verifying RL Formulas in Coq
Andrei Arusoaie

Configuration en langue naturelle du fonctionnement d'une maison intelligente
Driss Sadoun, Catherine Dubois, Yacine Ghamri-Doudane et Brigitte Grau

Evaluation de l’impact de fautes matérielles sur le logiciel par Model Checking
Didier Bassole, Jean-Louis Lanet et Axel Legay

Testium : outil de génération automatique de données de test pour les systèmes synchrones
Mouna Tka, Christophe Deleuze, Ioannis Parissis

Clôture de la journée AFADL

18h : Wine & Cheese

Mercredi 10 Juin - Journée GDR+AFADL

9h30-11h : Session commune avec le GDR : ouverture des journées, conférencier invité.
11h-13h : Session AFADL+GDR : Articles déjà publiés groupe de travail MFDL


Validation du standard RBAC ANSI 2012 avec B
Nghi Huynh, Marc Frappier, Amel Mammar, Régine Laleau et Jules Desharnais

Construction de programmes parallèles en Coq avec des homomorphismes de listes
Frederic Loulergue, Wadoud Bousdira et Julien Tesson

A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre et Frédéric Loulergue

Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
Andrei Arusoaie, Dorel Lucanu, David Nowak et Vlad Rusu

13h-14h : Déjeuner
14h-15h30 : Session AFADL + GDR : Articles déjà publiés groupe de travail MTV2


Instrumentation de programmes C annotés pour la génération de tests
Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov et Julien Signoles

Sound and Quasi-Complete Detection of Infeasible Test Requirements
Sebastien Bardin, Mickaël Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon et Jean-Yves Marion

Montre-moi d'autres contre-exemples : une approche basée sur les chemins
Kalou Cabrera Castillos, Helene Waeselynck et Virginie Wiels

15h30-16h : Pause café
16h-18h : GDR GPL - sessions démos et posters