[SMT-LIB] Open postdoc position at INRIA Saclay

[Claude Marche]

Hi all,

Here is an offer for a post-doc position that might be of interest for you.

- Claude

-------- Original Message --------
Subject: [gdr-im] Open postdoc position at INRIA Saclay
Date: Wed, 25 Aug 2010 13:14:10 +0200
From: Guillaume Melquiond <guillaume.melquiond at inria.fr>
To: gdr-im at gdr-im.fr

* Title

Designing an SMT theory for floating-point arithmetic

* Context

The ProVal team develops methods and tools for deductive verification of
behavioral properties of programs written in C and Java. The proof of a
property is done by generating verification conditions (VCs), which are
formulas to be shown valid by theorem provers. Alt-Ergo is an SMT
(Satisfiability Modulo Theory) solver designed by the team for
automatically proving such VCs.

One of the research topics of the team is the verification of numerical
programs. Due to the presence of floating-point arithmetic and
non-linear expressions, the generated VCs are out of the scope of the
theories built in Alt-Ergo. The use of dedicated tools such as Gappa can
alleviate this issue, but they only deal with the numerical fragment.
Some VCs may therefore fail to be proved by either tools, because they
mix symbols from several different domains.

* Description of work

In this study, we are interested in an SMT-friendly theory of
floating-point arithmetic. The postdoctoral student is expected to
design such a theory, possibly related to Gappa, and to implement it
into Alt-Ergo. Thanks to this combination of floating-point arithmetic
with the other existing theories, we hope to fully automatize the proof
of VCs generated by the Why framework for a large class of annotated
numerical programs.

The candidate will be located at INRIA Saclay-Île-de-France nearby
Paris. Net salary is about 2200 euros per month.

* Skills and Profile

Knowledge of SMT decision procedures.
Basic knowledge of floating-point arithmetic and program verification.
Programing skills in OCaml.

* Contact

Sylvain Conchon <sylvain.conchon at lri.fr>
Guillaume Melquiond <guillaume.melquiond at inria.fr>


-- 
Claude Marché                          | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Université                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |