[TYPES/announce] INRIA post-doc position on proof reconstruction from SMT solvers

[Stephan Merz]

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Stephan_Merz.vcf
Type: text/x-vcard
Size: 322 bytes
Desc: not available
Url : http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20090318/08ff56c5/Stephan_Merz-0001.bin