The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

A postdoctoral position is available within the TOCCATA (VALS) team, a 
computer science group between Inria Saclay Île-de-France and LRI (UMR 
8623 CNRS, University Paris-Sud 11). The position is funded by the ANR 
VERASCO research project, which investigates the formal verification of 
static analyzers and compilers.

The position is available starting September 2014 (with some flexibility 
on the starting date). Funding is available for one year and possibly a 
few more months; it does not extend past December 2015 though. It 
provides a net salary of around 2100 euros/month and standard benefits 
such as health insurance and social coverage. There are no teaching 
responsibilities.

* Description

This postdoctoral research is involved in the design of 
formally-verified methods for performing static analysis of 
floating-point programs. The goal is to write suitable decision 
procedures in the Coq proof assistant. Not only should these decision 
procedures be directly usable by the user as tactics for automatically 
discharging Coq goals, but it should also be possible to extract them to 
OCaml code. Indeed, we aim at plugging them into a framework for 
abstract interpretation of C programs built on top of the CompCert 
verified C compiler.

More precisely, the goal of this postdoctoral research is to develop a 
relational domain for floating-point arithmetic. Its implementation will 
have to be formally verified in Coq; but there is a trade-off to explore 
between an a priori verification (proving the algorithms themselves) and 
an a posteriori one (verification of generated certificates). Note that 
this abstract domain will focus only on the floating-point fragment of 
the C language; the ability to handle whole C programs will come from 
its integration with the other abstract interpreters from the framework.

* Application

The candidates should have a strong background in proof assistants and 
functional programing. Knowledge of floating-point arithmetic, abstract 
interpretation, and/or program verification, would be a plus.

Applications (in English or French) must include a cover letter 
highlighting the reasons for applying, a CV, a list of publications, a 
short summary of the Ph.D thesis (up to two pages), as well as names of 
at least three references with their email addresses. If the Ph.D. 
thesis is not yet defended, the candidate should provide the planned 
defense date. Application material must be sent to 
guillaume.melquiond AT inria.fr