[Coq-Club] Post-doctoral researchers wanted for Coq Developments @ VERIMAG

[David Monniaux]

VERIMAG has TWO open post-doc positions on Coq developments (certified
distributed algorithms; certified compiler)

- Contracts: for 12 months
- Location: Grenoble, France
- Hosting institution: VERIMAG laboratory (Université Grenoble Alpes,
CNRS Grenoble Institute of Technology)
- Scientific advisors: 1) Karine Altisen, Pierre Corbineau, Stéphane
Devismes
                       2) Sylvain Boulmé, David Monniaux


How to Apply & Contact Information

Please send information requests/applications to
***@univ-grenoble-alpes.fr
***@univ-grenoble-alpes.fr
***@univ-grenoble-alpes.fr
***@univ-grenoble-alpes.fr
***@univ-grenoble-alpes.fr

Email subject MUST start with "[Post-Doc Coq]"


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)

* Knowledge in 1) Distributed Algorithms or 2) Compiler Internals is a plus

Coq is a proof assistant mixing software development in a purely
functional strongly-typed language and theorem proving.


VERIMAG is a leading laboratory in methods for the development of
safety-critical systems. There are several ongoing efforts at VERIMAG on
Coq proofs, including one on distributed algorithms and one on certified
compilers.


1) Distributed systems must tolerate faults. 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. We are
currently developing a framework called PADEC
(http://www-verimag.imag.fr/~altisen/PADEC/), based on Coq, to (semi-)
automatically construct certified proofs of self-stabilizing algorithms.
We import into Coq the computational model in which the targeted
algorithm is designed, formalize the algorithm itself and then prove
that it respects its specification (safety, convergence, and some
performance criteria).


2) The CompCert compiler (http://compcert.inria.fr/) is proved to
compile C programs while preserving their semantics. Each transformation
or optimization phase comes with a proof of preservation of semantics.
It has backends for various processors, including RiscV. VERIMAG is to
develop and prove correct a backend for a secure variant of RiscV, in
collaboration with the developers of that processor.