The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

==============================================================================

At the INRIA Futurs (Orsay, France), a postdoc position for one year
is available in the ProVal project, devoted to

  Functional Interpretation of C Functions

Starting date of this Postdoc position: September 2007

==============================================================================

Context: 
  The ProVal project is developing the tool Caduceus for the
  formal verification of behavioral properties of C programs at the
  source level (http://caduceus.lri.fr/). It is based on a classical
  Hoare Logic framework where programs are annotated with pre- and
  postconditions and loop invariants.

Description of the postdoc activity:
  To be modular, Hoare Logic requires each function to be given a
  postcondition describing the computation it performs. Most of the
  time, this postcondition appears to be an abstraction of the
  function's code. In some cases, however, the postcondition is simply
  rephrasing the code, which constitutes both a duplication of the
  code and a useless proof search.

  The aim of this work is to design and implement a method to
  automatically associate a postcondition to some particular C
  functions (to be identified), as a functional interpretation of
  their codes. We will start with simple functions performing only
  tests and computations on local variables. Then we will extend it to
  side-effects on global variables. Finally, we will study the case of
  loops where the functional interpretation could be expressed as
  inductive relations.

  This work will be part of the RNTL project CAT (C Analysis Toolbox)
  and its results will be directly applied to industrial critical code.

Required knowledge and competences:
  - notions of formal methods (especially Hoare Logic)
  - programming skills with the languages C and Objective Caml

==============================================================================

For further information about this position please contact

  Jean-Christophe.Filliatre at lri.fr