Job opportunity at INRIA Sophia Antipolis

[The position involves substantial work with type-theory based
proof-development systems and may therefore be of interest to
the TYPES readers.]


INRIA Sophia-Antipolis opens one 1-year position in the Oasis team.
The position is connected to Formavie, a joint project between Bull,
Schlumberger and INRIA, and partially supported by the French Ministry
of Economy, Finances and Industry.

The goal of Formavie is to provide secure embbeded software for the
success of electronic commerce.  The role of INRIA in Formavie is to
provide formal tools and methodology to ensure security for embedded
software and in particular smartcards and terminals. The main task
involved is the design and development of a toolset for the
formalization, analyzis, transformation and visualization of models of
embedded systems (virtual machines) and security policies for those

The position offers opportunities for innovative and collaborative
research in the area of formal verification as well as for developing
applications to be used in an industrial context, with a challenging
goal: achieving for the embedded systems a high-level of certification
(EAL7) w.r.t. common criteria (See http://csrc.nist.gov/cc).

We welcome applicants with a strong background/interest in formal
methods, especially in formal verification (theorem-proving,
model-checking, etc) and program analysis/transformation, and a strong
interest in smartcard security.

See http://www.inria.fr/oasis/Formavie
For further information, please contact Isabelle Attali.

The deadline for applications is September, 15th 2000. Applications
must include a cv, (pointers to) relevant publications and the names
and addresses of two referees.  Applications should be addressed to:

Isabelle Attali
INRIA Sophia Antipolis
2004 Route des Lucioles
BP 93
06902 Sophia Antipolis Cedex
TÚl: +33 (0)4 92 38 79 10
Fax: +33 (0) 4 92 38 76 44