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.
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 well suited 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@inria.fr
guillaume.melquiond@inria.fr
urbain@lri.fr
Salary: 2 607,80 € gross/month
Today's Conversion Quote:
U$ 3581.55 gross/month
Administrative informations: rachel.norvez@inria.fr
How to apply (*before 31 March*):
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html
1 comment:
I have no clue whatsoever, maybe this helps to clarify matters
http://en.wikipedia.org/wiki/Random_matrix
I seem to remember that Andcrew Wiles used this sort of thing to solve the Fermant mistery.
As for the money they offer, not bad for an Euro country (I used to make more at my regular office job, but we'll quietly skip that one over).
Post a Comment