Obtaining certified guarantees for distributed systems is a crucial issue, as this area of computer science is well-known for being remarkably harsh on informal reasoning, which potentially leads to disastrous errors. In practical cases, the number of slight variants of the original computation model, the difficulty to reuse previous results, even when obtain under very close assumptions, make the validation process a challenging task with formidable technical difficulties.
The need for formally verified grounds is even stronger when the models under study are emerging, and developing fast.

FURETHERMORE focuses on two aspects of recent models: Mobility & Redundancy, two important keywords in today's massively computerised and data-eager environment.

In particular, it addresses formal verification techniques well-suited to: 

• Swarms of autonomous mobile robots, which have to cooperate to achieve complete tasks, possibly of critical importance, in a potentially hostile environment; the system is highly dynamic as they may have to reorganise to face failures, either crash or Byzantine.
• No/NewSQL-like Database Management Systems, which are nowadays the norm when it comes to Big Data management, a demanding context that requires several machines, if only for storing raw data, and where expected guarantees on behavioural properties may include Data (eventual-)consistency, availability, and partition resilience.

Following the 2017 edition of MoRoVer, FURETHERMORE, workshop colocated with SRDS, addresses the development and application of formal methods in such contexts. It aims to bring together researchers from academia and industry, specialists of distributed computing or formal methods, as well as students, for scientific presentations, and tutorials.


The morning and early afternoon are dedicated to scientific presentations :

• First talk: 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.

The afternoon offers the opportunity for tutorials (students welcome!) about different verification techniques.