Email Gateway (Aug 18 2022 at 10:19): Email Gateway (Aug 18 2022 at 10:19):From: Leonor Prensa <leonor.prensa@loria.fr>
**
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@loria.fr
Leonor Prensa Nieto: +33 383 59 30 75, Leonor.Prensa@loria.fr
Last updated: May 03 2024 at 04:19 UTC