[isabelle] Post-doc position at LORIA, Nancy (France)



**

Research team: MOSEL team at INRIA Lorraine, LORIA (http://www.loria.fr/)
/
INRIA proposes post-doctoral positions for young graduates to a maximum of two years.
The salary is 2,320€ gross per month.
/
Research subject: Proof traces and proof reconstruction for automatic and interactive provers

Research context :

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.

Description of the activity of the post-doc :

The post-doctoral researcher will investigate techniques for
• improving our existing combination techniques. Some care will be directed to efficiency for the certification of large proofs: proof obligations arising from verification problems can be large, and interactive proof assistants are typically not optimized for representing large formulas. A promising approach may be to use reflection techniques to produce a verified certification tool. • extending the combination techniques beyond the fragments of first-order logic that are currently handled, and in particular to take into account decidable fragments of arithmetic reasoning. In order to obtain a comprehensive framework, the exchange of proofs should be based on a general-purpose format for representing formal proofs; we are involved in an international standardization effort in which the post-doc will naturally participate. The developed techniques will be evaluated by applying them on theories that are already supported by haRVey or for which support is currently being implemented – with a particular interest for arithmetics – but also by using them for the integration of generic first-order logic automatic provers such as Spass or the E-prover. We mainly think of Isabelle as the targeted proof assistant, but application to other interactive frameworks, such as Coq, would be useful, also as a means to demonstrate that the technique is independent of a specific proof assistant. Finally, it will be important to measure the improvement brought by the combination of deductive tools on real case studies; our main interest is in the verification of distributed algorithms, including communication protocols for embedded systems such as FlexRay. The research directions mentioned above are indicative of our interests in this field; the precise subjects of research will be determined jointly with the candidate. Part of this work will be carried out in close contact with the Isabelle group in Munich and with other international research teams.

Competences and profile :

The candidate should 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. The candidates must have defended their doctoral thesis between May 2006 and end of 2007.

Contact :

Candidates should send a resume to

Pascal Fontaine: +33 354 95 84 78, Pascal.Fontaine at loria.fr
Leonor Prensa Nieto: +33 383 59 30 75, Leonor.Prensa at loria.fr






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.