[TYPES/announce] Post-doctoral position at VERIMAG, Grenoble, France

[Radu Iosif]

[Apologies for multiple postings]

The VERIMAG laboratory has a vacancy for a post-doctoral position on:

        Development of Automatic Techniques for Software Verification
        =========================================

*** Project description

The goal of this project is the verification of C programs that are
used to control safety-critical systems, such as power plants. A major
problem is the scalability of existing verification techniques for
programs with dynamic data structures. These techniques are capable
nowadays of analyzing and finding bugs in toy programs of about 100
lines of code. In this project we aim, on one hand, at extending the
existing verification techniques in order to deal with parallel
programs handling singly-linked lists and array data structures. On
the other hand, we aim at applying these techniques to real-life test
cases, with sizes of several tens of thousands lines of C code.

*** Research group

The research will take place in the Distributed and Complex Systems group
(http://www-verimag.imag.fr/~async/pv.html) of the research laboratory
VERIMAG. The members of this group focus on a wide range of problems such
as program verification, computer security, testing and synthesis, 
component-based
development, etc. VERIMAG is an academic research laboratory affiliated 
with CNRS
(French National Research Center), UJF (University Joseph Fourrier) and 
INPG
(National Polytechnic Institute of Grenoble).  

*** Qualifications

The applicants must have a PhD in Computer Science, with knowledge in
at least one of the following fields:

- logics, proof theory, arithmetic theories, linear integer programming
- formal languages, automata theory
- deductive or algorithmic verification (model checking)

*** Job description

The appointment is for one year, starting as soon as possible, with
possibility of extension. The contract will be within the VERIDYC
project of the ANR (French National Research Agency).

More information at: http://www-verinew.imag.fr/VERIDYC.html

The chosen candidate is expected to work on the implementation of a
prototype using the Frama-C framework: http://frama-c.cea.fr/

Knowledge of the French language is not required.

*** Contact

For further information and applications, send email to Radu.Iosif at imag.fr