The Coq mailing list

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

A postdoctoral position is available within the TOCCATA 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 2013 (with some flexibility
on the starting date). Funding is available for 23 months and 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 analyzing floating-point programs. The goal is to write
suitable decision procedures in the Coq proof assistant, while keeping
the following two objectives in mind. First, they should be directly
usable by the user as tactics for automatically discharging Coq goals.
Second, it should be possible to extract them to OCaml code so that they
can be plugged into the CompCert verified C compiler, and thus can be
used for static analysis of C programs.

The starting point would be the Gappa tool. It is dedicated to the formal
verification of the arithmetic properties that occur inside numerical
codes, e.g. variable bounds and error analysis. This tool is currently
written in C++ and, to ensure that its analyses are correct, it generates
a formal proof that can be checked by Coq. (It can also be directly
called from Coq as a tactic.) This approach has a few downsides. First,
it requires Gappa to keep track of all its computations so as to be able
to build the proof, which incurs a noticeable memory footprint. Second,
while Gappa analyses are often instant, checking the generated proofs
with Coq can take hours for medium-sized programs.

The solution to these issues is to move from an a posteriori Coq
verification of Gappa's results to an a priori Coq verification of the
tool itself. In other words, the critical parts of Gappa would be moved
from C++ to Coq so that they can be proved once and for all and so that
proof generation becomes superfluous. The Coq tactic would no longer
depend on an external proof generator, while Gappa would become a
self-contained tool extracted from the Coq code. This work will also
offer the opportunity to design and implement new methods for verifying
state-of-the-art floating-point functions, as found in mathematical
libraries.

Later on, the work will aim at developing new Coq decision procedures for
formally-verified static analyzers for C programs. These analyzers are
based on abstract interpretation. Again, there is a trade-off to explore
between a priori and a posteriori formal verification. For instance, the
narrowing and widening operators for finding program invariants do not
have to be proved in their entirety, only their results have to. The
scope of these decision procedures is not set yet; it will depend on
which abstract domains are implemented during the course of the VERASCO
project. The postdoctoral researcher is, however, expected to take part
into the related discussions.

* Application

The candidates should have a strong background in proof assistants and
functional programing. Knowledge of floating-point arithmetic, error
analysis, 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