[TYPES/announce] Postdoc position available at VERIMAG, France

[Radu Iosif]

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

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


*** Project description

Within the past decade, push-button verification techniques (e.g. model
checking, SAT solving, etc.)
have become commonplace in the development of hardware systems. An
integration of such methods
with software development is highly required by the manufacturers of
critical and embedded software
(avionics, telecom, public transport, etc.). However, the rather
sophisticated nature of software
(complex data structures, recursion, multithreading) pose interesting
theoretic and practical problems
to the developers of automatic analysis and verification methods.

The goal of this project is to adress concrete verification problems
of real-life software. Research areas include, but are not limited to:

- program logics and proofs
- generation of invariants
- infinite-state model checking
- static analysis (abstract interpretation)

The appointment is for one year, starting as soon as possible, with
possibility of extension.

The contract will be within the AVERILES project of the ANR (French
National Research Agency):
http://www.lsv.ens-cachan.fr/rntl-averiles/

*** 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:

- first-order, higher-order logics, proof theory, arithmetic theories
- formal languages, automata theory, rewriting

Previous experience in the domain of verification is not required, but
may be considered a plus. Knowledge
of the French language is not required.

*** Contact

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