[TYPES/announce] Postdoctoral position available at Université Grenoble Alpes, France

[Pierre Corbineau]

We have a Postdoctoral position currently available.

Subject: Formal proofs (using Coq) for Distributed Algorithms

- Position: Post-Doctoral researcher
- Contract: 12 months
- Starting date: Sept-Dec 2020
- Location: Grenoble, Auvergne-Rhône-Alpes, France
- Hosting institution: VERIMAG laboratory, Université Grenoble Alpes,
Grenoble Institute of Technology
- Scientific advisors: Karine Altisen, Pierre Corbineau, Stéphane Devismes

How to Apply & Contact Information

Please send information requests/applications to
Karine.Altisen at univ-grenoble-alpes.fr,
Pierre.Corbineau at univ-grenoble-alpes.fr,
Stephane.Devismes at univ-grenoble-alpes.fr

Email subject MUST start with "[Post-Doc PADEC]">

Applications must include the following documents:
- Letter of application: why you are interested in this research
  position and what you would like to work on
- Curriculum vitae
- References or letters of recommendation
- Applicant’s scientific report or paper written in English
- Any other document showing that you are an outstanding candidate

Required Skills

- Software Development
- Theorem Proving (preferably with Coq)
- Distributed Algorithmic is a plus

Subject

Modern distributed systems can be large-scale (e.g., Internet),
dynamic (e.g., Peer-to-Peer systems), and / or resource
constrained (e.g., wireless sensor networks (WSNs)). Those
characteristics increase the number of faults which may hit the
system. For instance, in WSNs, processes are subject to crash
failures because of their limited battery. Moreover, their
communications use radio channels which are subject to
intermittent loss of messages. Now, due to their large-scale and
the adversarial environment where they may be deployed,
intervention to repair them cannot be always envisioned. In this
context, fault-tolerance, i.e., the ability of a distributed
algorithm to endure the faults by itself, is mandatory.
Self-stabilization is a versatile lightweight technique to
withstand transient faults in a distributed system. After
transient faults hit and place the system into some arbitrary
global state, a self-stabilizing algorithm returns, in finite
time, to a correct behavior without external
intervention. Self-stabilization makes no hypotheses on the
nature or extent of transient faults that could hit the system,
and recovers from the effects of those faults in a unified
manner.  Today's researches on self-stabilizing algorithms focus
on more and more complex problems and adversarial
environments. This makes the proof that an algorithm actually
achieves self-stabilization even more complex and subtle to
establish. Now, those proofs are usually performed by hand, using
informal reasoning.  Such methods are clearly pushed to their
limits and this justifies the use of a proof assistant.

Proof assistants are environments in which a user can express
programs, state theorems, and develop proofs interactively, those
ones being mechanically checked (i.e., machine-checked). In
particular, the Coq proof assistant, which is targeted by this
project, has been successfully used for various tasks such as
mathematical developments as involved as the 4-colors or
Feit-Thompson theorems, formalization of programming language
semantics leading to the certification of a C compiler, certified
numerical libraries, and verification of cryptographic protocols.
Project. We propose a framework called PADEC, based on Coq, to (semi-)
automatically construct certified proofs of self-stabilizing
algorithms. The framework is currently under development and a
first experiment has been conducted, with the certification of a
non-trivial case study. This work imports into Coq the
computational model in which the targeted algorithm is designed,
formalizes the algorithm itself and its specification.  Then the
algorithm is proved using Coq including safety, convergence and
also some performance analyses.

This postdoc aims at further developping the PADEC library, a
library of tools in Coq to handle the certification of
self-stabilizing algorithms.