# [isabelle] INRIA post-doc position on proof reconstruction from SMT solvers

`As part of INRIA's 2009 campaign for recruiting post-doctoral
``researchers, the Mosel team in Nancy is looking to hire somebody on the
``topic:
`

`Efficient proof synthesis, compression and reconstruction of proofs from
``SMT solvers
`

`The objective of our work is the construction of a verification
``environment that integrates 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, we are interested in a skeptical
``approach to combining reasoners. We rely on automated reasoning tools
``that produce justifications which can be 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 gained some initial experience with this approach
``when we combined Isabelle/HOL with SAT solvers and with the SMT solver
``haRVey (the ancestor of our solver, veriT) for fragments of first-order
``logic, including equality reasoning. However, many research questions
``remain open in order to make that idea scale to industrially relevant
``verification problems. The goal of the post-doctoral research proposed
``here is to address some of the scientific and technological issues in
``order to make the approach more robust, efficient, and scalable.
`

`Proof generation and certification need to be extended beyond the
``fragments of first-order logic that we can currently handle. In
``particular, proofs of Skolemization, quantified theories, and arithmetic
``(over the integers, reals, and potentially bit vectors) must be
``included; extensions to fragments of higher-order logic are also of
``interest. We are aiming at the definition of a generic and extensible
``proof format that is independent of a specific automatic prover and
``interactive proof assistant.
`

`The issue of scalability is of concern because proof obligations that
``arise from verification problems are often large formulas, usually in
``restricted first-order theories; correspondingly, they generate long
``proofs. Modern automatic provers are optimized for handling such
``formulas, but interactive proof assistants focus primarily on
``expressive, higher-order logical languages, for which elementary
``problems such as unification or matching are computationally expensive.
``A promising approach may be to explore reflection techniques in order to
``produce a verified and efficient proof certifier. On a more theoretical
``level it will be interesting to investigate the trade-off between
``generating a fully detailed proof, which is easy to check but large, and
``a more compact proof certificate that guides certification but requires
``the certifier to regenerate parts of the proof. For example, decision
``procedures for certain fragments of arithmetic are so efficient that it
``will certainly be preferable to let the certifier recreate a proof of
``sub-formulas falling into such fragments. Little is known about the
``proof sizes for first-order theories in general, and reconstruction of
``such proofs from compact certificates.
`

`The research on proof representation and certification should be
``validated by an implementation for combining veriT, and possibly Spass,
``with Isabelle and Coq. In this way, the added value of using an
``integrated verification tool can be measured, and practical experiences
``with the proposed proof format can be performed. Our main interest is in
``the verification of distributed algorithms, including TLA+
``specifications of concurrent algorithms.
`

`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
``contact with the Isabelle group in Munich, with our partners of the ANR
``project DECERT, the TLA+ prover project at the INRIA-MSR joint lab, and
``with other international research teams.
`

`The candidate must have experience in interactive and/or automatic
``theorem proving. He or she should be interested in combining
``foundational research on calculi and logics with hands-on
``implementation. The main languages of implementation are C and ML.
`
Further details:
Duration: 12 months
Starting date: Between 1 Oct 2009 and 31 Dec 2009
Working place: INRIA Nancy & LORIA, equipe Mosel
The position is an INRIA-postdoc position and candidate must fulfill
the formal requirements found at
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html.

`In particular, the candidate should have defended a doctorate or Ph.D.
``in May 2008 or later. If the Ph.D. is not defended at the application
``date, you should clearly point out the defense date and the composition
``of thesis jury.
`

`Applications should be made via the above web site before June 30, 2009.
`` Late applications may also be considered if the position is not filled.)
`

`Please contact Stephan Merz (Stephan.Merz at loria.fr) and/or Pascal
``Fontaine (Pascal.Fontaine at loria.fr) for details about the position.
`begin:vcard
fn:Stephan Merz
n:Merz;Stephan
org:INRIA Nancy & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at loria.fr
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79
x-mozilla-html:FALSE
url:http://www.loria.fr/~merz/
version:2.1
end:vcard

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