The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

INRIA Saclay--Île-de-France (Paris area) is offering a postdoctoral 
position of up to 24months on certified automated termination of linear 
programs.

Environnement
Proving termination is a crucial issue when it comes to formal proof of
programs. It marks, for instance, the boundary between partial and total
correctness. Termination proofs are always difficult to find, and
there is a growing need for automating their discovery, in particular
in the context of proof assistants, like Coq.
There has been recently an increasing effort towards certification of
automated proof of termination, effort in which the ProVal team was
particularly involved through the A3PAT project 
(http://a3pat.ensiie.fr), regarding first-order
term rewriting. A major topic in the ProVal team is the
development of tools for the formal verification
of programs (C or Java), that is, imperative style programs.
Semi-decision procedures for termination are very important here,
especially if their results can be certified by a proof assistant.

Missions:
In this proposal, we aim to automate and to
certify termination proofs for 'while' loops, with convex
guards and linear assignments over real numbers. To this goal, we want
to use Tiwari's approach (Termination of Linear Programs, CAV'04), based 
on the analysis of eigenvalues and
eigenvectors of the assignment matrix, on topology results,
and on fixpoint theorems.
The planned work is to formalise this approach in the Coq proof
assistant, possibly weakening its premises, and to link that
formalisation with an automated prover dedicated to termination.

Activities:
A first part of the work is to devise efficient
formal models of matrices over R, and of notions of compact
spaces, convex functions, etc., as well as special instances of
Brouwer's theorem. This part will be done in close collaboration with
the INRIA team TypiCal. It is worth noticing that such
formalisations often yield new results, in particular by pointing out
premises that are too strong or restrictive.
A second part of the work is to automate the analysis and to generate
proof traces that can be certified using the formal development above.
This can be done as an extension of the A3PAT framework. Thus, a key
point will be to keep the formal models wellsuited for a use in
conjunction with automated provers.

Expected skills:
The candidate will have a strong mathematical background, as well as
in formal methods, preferably with the Coq proof assistant.
An experience with formal proofs regarding real analysis would be a 
clear plus

Location:
Centre de recherche Inria Saclay-Île-de-France
ProVal Team: http://proval.lri.fr/
TypiCal Team: http://www.lix.polytechnique.fr/typical/

Scientific contacts:
assia.mahboubi AT inria.fr,
 
guillaume.melquiond AT inria.fr,
 
urbain AT lri.fr

Salary :
2 607,80 € gross/month

Administrative informations:
rachel.norvez AT inria.fr

How to apply (*before 31 March*):
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html