Email Gateway (Aug 18 2022 at 13:12): Email Gateway (Aug 18 2022 at 13:12):From: Stephan Merz <Stephan.Merz@loria.fr>
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@loria.fr) and/or Pascal
Fontaine (Pascal.Fontaine@loria.fr) for details about the position.
Stephan_Merz.vcf
Last updated: May 03 2024 at 04:19 UTC