The Coq mailing list

[David Monniaux <David.Monniaux AT univ-grenoble-alpes.fr>]

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
Karine.Altisen AT univ-grenoble-alpes.fr
Pierre.Corbineau AT univ-grenoble-alpes.fr
Stephane.Devismes AT univ-grenoble-alpes.fr
Sylvain.Boulme AT univ-grenoble-alpes.fr
David.Monniaux AT 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.

-- 
David Monniaux
directeur de recherche au CNRS, laboratoire VERIMAG
Université Grenoble Alpes
http://www-verimag.imag.fr/~monniaux/

begin:vcard
fn:David Monniaux
n:Monniaux;David
org:CNRS;VERIMAG
adr;quoted-printable;quoted-printable:700 avenue Centrale;;VERIMAG, universit=C3=A9 Grenoble Alpes, b=C3=A2timent IMAG;Saint Martin d'H=C3=A8res;;38401;France
email;internet:David.Monniaux AT univ-grenoble-alpes.fr
title:directeur de recherche
tel;work:+33 4 57 42 22 32
tel;fax:+33 4 57 42 22 22
note;quoted-printable:GnuPG=0D=0A=
	pub   4096R/C371AAD0 2017-01-13 [expires: 2022-01-12]=0D=0A=
	 Key fingerprint =3D D671 CC22 03A6 5156 1C32  9AC4 A3C2 E122 C371 AAD0
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~monniaux/
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature