[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
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.
fn:Stephan Merz
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

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