| MERCREDI |
| S1 – MFDL – AFSEC |
| 11h00 |
Julien Brunel, David Chemouil and Jeanne Tawa |
Une analyse de la propriété fondamentale de vivacité du protocole Chord |
| 11h30 |
Guillaume Dupont, Yamine Ait Ameur, Marc Pantel and Neeraj Singh |
Approches au Développement Formel de Systèmes Hybrides Basées sur la Preuve : Logique Dynamique et Event-B |
| 12h00 |
Yves Ledru, Akram Idani, Rahma Ben Ayed, Abderrahim Ait Wakrime and Philippe Bon |
Une approche basée sur la séparation des préoccupations pour modéliser et vérifier les règles de signalisation d'un système ferroviaire |
| S2 – LTP |
| 16h30 |
François Pottier (invité) |
On est tranquilles pour longtemps -- les reçus-temps en logique de séparation |
| 17h00 |
Érik Martin-Dorel and Pierre Roux (invités), Guillaume Bertholon |
Primitive Floats in Coq |
| 17h30 |
Florian Faissole |
Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels |
| JEUDI |
| S3 – MTV2 |
| 11h00 |
Helene Waeselynck |
Test d’un robot agricole en simulation |
| 11h30 |
Jean-Philippe Gros |
Tests de politiques d'adaptation pour systèmes cyber-physiques |
| 12h00 |
Burkhart Wolff (invité) |
Towards a Test-and-Proof Framework for C11 in Isabelle/HOL |
| S4 |
| 14h00 |
Gabriel Radanne, Anil Madhavapeddy, Jeremy Yallop, Thomas Gazagnaire, Richard Mortier, Hannes Mehnert, Mindy Preston and David Scott |
Ingénierie dirigée par les foncteurs |
| 14h30 |
Christophe Chareton, Sebastien Bardin, François Bobot, Valentin Perrelle and Benoît Valiron |
Qbricks, un environnement pour la vérification formelle en informatique quantique |
| 15h00 |
Jessy Colonval and Henri de Boutray |
Formalisation et validation d'une méthode de construction de systèmes de blocs |
| 15h30 |
Nasrine Damouche, Xavier Thirioux, Matthieu Martel and Hanane Benmaghnia |
Dépliage de Boucles Versus Précision Numérique |
| S5 |
| 16h30 |
Allan Blanchard, Nikolai Kosmatov and Frederic Loulergue |
La logique contre les fantômes: comparaison de deux approches pour la preuve d’un module de listes chaı̂nées |
| 17h00 |
Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov, Arnault Lapitre and Stéphane Louise |
Polygraph: un modèle flot de données avec arithmétique de fréquences |
| 17h30 |
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling and Pascale Le Gall |
MetAcsl : spécification et vérification de propriétés de haut niveau |
| VENDREDI |
| S6 |
| 09h00 |
Pascal Béger, Valentin Becquet, Sebastien Leriche and Daniel Prun |
Contribution à la formalisation des propriétés graphiques des systèmes interactifs pour la validation automatique |
| 9h30 |
Khaled Khebbeb, Nabil Hameurlain and Faiza Belala |
Formalisation, vérification et évaluation de stratégies d'élasticité dans le Cloud |
| 10h00 |
Valentin Besnard |
Unification de la Vérification et de l’Exécution Embarquée de Modèles |
| S7 |
| 11h00 |
Valentin Besnard, Matthias Brun, Philippe Dhaussy, Frédéric Jouault and Ciprian Teodorov |
EMI : Un Interpréteur de Modèles Embarqué pour l’Exécution et la Vérification de Modèles UML |
| 11h30 |
Steve Jeffrey Tueno Fotso (20m) |
Modélisation du Domaine au Sein d’une Méthode Formelle d’Ingénierie des Exigences |
| 11h50 |
Marion Kissous, Thomas Lambolais, Anne-Lise Courbis, Gérard Dray and Sophie Martin (20m) |
Spécification incrémentale d'un système d'aide au diagnostic de l'épuisement professionnel : problématique et revue de littérature |
| 12h10 |
Lilian Burdy, David Déharbe and Ronan Saillard (20m) |
Intégration d'outils tiers de preuve automatique dans Atelier B |
