16 March 2010
Vleeptron is pleased to offer 1 paid year in Paris / address all questions to ANYBODY BUT Vleeptron
INRIA Saclay--Île-de-France (Paris area) is offering a postdoctoral position of up to 24 months on certified automated termination of linear programs.
Environment 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.
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.
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 well suited for a use in conjunction with automated provers.
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.
Centre de recherche Inria Saclay-Île-de-France
ProVal Team: http://proval.lri.fr/
TypiCal Team: http://www.lix.polytechnique.fr/typical/
Scientific contacts: firstname.lastname@example.org
Salary: 2 607,80 € gross/month
Today's Conversion Quote:
U$ 3581.55 gross/month
Administrative informations: email@example.com
How to apply (*before 31 March*):