Dans le contexte des systèmes distribués, obtenir des garanties sur la sûreté des programmes est crucial : ce domaine de l'informatique est bien connu pour son intransigeance face aux imprécisions et aux raisonnements  informels, lesquels peuvent introduire des erreurs subtiles mais aux conséquences désastreuses. En pratique, les nombreuses--et les plus légères--variantes du modèle de calcul initial et la difficulté de réutiliser des résultats antérieurs même sous des hypothèses très proches font de la validation un défi extraordinairement complexe sur le plan technique.

Bénéficier de bases garanties formellement est une nécessité, rendue d'autant plus évidente que le domaine est émergent et en rapide expansion.

FURETHERMORE s'intéresse plus particulièrement à deux aspects de modèles émergents : la mobilité et la redondance, deux notions incontournables dans le monde d'aujourd'hui, largement informatisé et qui  dépend de données massives comme jamais auparavant.

Le colloque est ainsi consacré aux techniques de vérification formelle adaptées aux :

• Essaims de robots mobiles : devant coopérer afin de réaliser des tâches complexes et potentiellement critiques dans un environnement considéré comme hostile, ils constituent un système extrêmement dynamique devant savoir se réorganiser en cas de fautes de différents types (crash, byzantines...).
• Systèmes de gestion de données de type No/NewSQL : aujourd'hui la norme pour la gestion des données massives, ils opèrent dans un contexte requérant de nombreuses machines, ne serait-ce que pour le stockage des informations, et dont on attend différentes propriétés telles que la cohérence (éventuellement à terme), l'accessibilité des données et la robustesse à la partition.

À la suite du l'édition 2017 du colloque MoRoVer, FURETHERMORE, cette année workshop colocalisé avec SRDS,  s'intéresse au développement et à l'application de méthodes formelles dans ces contextes. Il vise à rassembler chercheurs académiques et industriels, spécialistes d'algorithmique distribuée ou de méthodes formelles, et bien sûr étudiants, autour d'exposés scientifiques et de tutoriels ouverts.

La matinée et le début d'après-midi sont consacrés aux exposés :

• Exposé d'ouverture : Sergio Rajsbaum (Universidad Nacional Autonoma de Mexico).
  • Indistinguishability and its importance in distributed computing and formal methods

• Véronique Benzaken (Paris-Saclay),     Toward a Coq-verified SQL compiler,
• Xavier Défago (Tokyo-Tech),      Model-Checking Robot Algorithms in Euclidean Space,
  
• Toshimitsu Masuzawa (Osaka University),     Loose-stabilization in the population protocol model,
• Sébastien Tixeuil (Sorbonne Université),    Quantifying "eventual" in eventual correctness by probabilistic model checking.
  

L'après-midi propose des tutoriels sur différentes approches formelles.