The Coq mailing list

[Pascal Fontaine <Pascal.Fontaine AT loria.fr>]

A two years INRIA Post-doctoral position (Loria, Nancy, France) is 
available.

Title: Proof traces and proof reconstruction for automatic and 
interactive provers

Missions (goals of this work) :
The objective of our work is the construction of a verification 
environment that combines specialized automated reasoners within an 
interactive reasoning framework. We intend to demonstrate that one can 
in this way significantly raise the degree of automation for the 
verification of complex systems and thus contribute to make deductive 
verification techniques economically viable. In order to ensure the 
overall correctness of a proof, the automated reasoning tools produce 
justifications that are certified by the interactive proof assistant. In 
this way, both the result of the external reasoner and the translations 
between the different syntactic representations are verified. Contrary 
to proof search, proof checking is of low polynomial complexity. We have 
validated this approach by combining Isabelle with SAT solvers and with 
the SMT solver haRVey for fragments of first-order logic, including 
equality reasoning. The goal of the post-doctoral research proposed here 
is to extend the approach, to make it more robust, and to improve the 
efficiency.

Competences and profile : The candidate must have experience in 
interactive and, if possible, automatic theorem proving, and should be 
interested in combining foundational research on calculi and logics with 
hands-on implementation. The main languages of implementation are C and ML.

More information about the subject : 
http://www.loria.fr/equipes/mosel/jobs/proofreconstruction/index.html

More information about INRIA post-doctoral positions: 
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html

Application deadline: March 31, 2007.

Application information : on-line application on 
http://www.talentsplace.com/syndication1/inria/ukpostdoc/details.html?id=PNGFK026203F3VBQB6G68LOE1&LOV5=4508&LOV6=4514&LG=EN&Resultsperpage=20&nPostingID=1149&nPostingTargetID=3188&option=52&sort=DESC&nDepartmentID=19

Contact information : 
Pascal.Fontaine AT loria.fr,
 
Leonor.Prensa AT loria.fr