The Coq mailing list

[David Nowak <david7nowak AT gmail.com>]

The 2XS team at Univ. Lille & CNRS, France
(http://cristal.univ-lille.fr/2XS/) is proposing a funded postdoctoral
position in the area of formal methods for system-level security. The
duration of the post is 18 months, starting as soon as possible and no
later than January 2017. The gross salary is about 2600 euros/month.
Standard social benefits (e.g., health insurance) are included.
Knowledge of French is not required.

Scientific context:

Within the ODSI project (https://www.celticplus.eu/project-odsi/) we
are developing a microkernel called Pip whose main role is to ensure
memory isolation properties between different system components. A
reference implementation of Pip has been written in the language of
the Coq proof assistant. A C version of Pip is automatically generated
by translating the Coq implementation into a subset of C. The question
that naturally arises is whether the memory-isolation properties,
which are being proved to hold on the Coq version, still hold in the
translated C version. That is the question that the postdoc will be in
charge of investigating.

More specifically, the Coq version of Pip is written in an imperative
style, using a state monad. A Hoare logic has been developed on top of
the monad. The memory-isolation properties are thus written in Hoare
logic. In order to prove the correctness of the translation one may
proceed as follows: 1. define a way of formalising properties of code
written in the considered subset of C; 2. define a translation of
properties from the Coq level to the C level; and 3. prove that
translated formulas holds on translated C code whenever the
corresponding original formulas hold on the original Coq code.

The candidate is expected to develop a general, sound theory, possibly
(but not necessarily) along the lines sketched above. He/she is also
expected to implement the theory in tools and to apply the tools on
case studies - in particular (but not exclusively) on our Pip case
study.

Qualifications: PhD in Computer Science, either already defended or to
be defended soon. Experience in formal methods (program verification
and proof assistants) is essential for the successful candidate.

Contact: 
David.Nowak AT univ-lille1.fr,
 
Vlad.Rusu AT inria.fr