[Prev][Next][Index][Thread]
PhD grant at INRIA Sophia Antipolis
-
To: amast@cs.utwente.nl, asci@twi.tudelft.nl, bra-types@cs.chalmers.se, calculemus-ig@dist.unige.it, categories@mta.ca, ccl@dfki.uni-sb.de, compunode@compulog.org, concurrency@cwi.nl, coq-club@pauillac.inria.fr, cs-logic@cs.indiana.edu, dataloger@cs.chalmers.se, eacsl@dimi.uniud.it, facs@lboro.ac.uk, formal-methods@cs.uidaho.edu, fsdm@it.uq.edu.au, ftp@logic.at, info-hol@jaguar.cs.byu.edu, isabelle-users@cl.cam.ac.uk, kgs@logic.tuwien.ac.at, lics-request@research.bell-labs.com, linear@cs.stanford.edu, logic-ml@logic.jaist.ac.jp, lprolog@central.cis.upenn.edu, mizar-forum@mizar.uwb.edu.pl, mop@cs.ruu.nl, ozsl-list@fwi.uva.nl, protagonist@cs.kun.nl, qed@mcs.anl.gov, rewriting@ens-lyon.fr, theorem-provers@ai.mit.edu, theorynt@listserv.nodak.edu, types@cis.upenn.edu, alp-diffusion@univ-lille1.fr
-
Subject: PhD grant at INRIA Sophia Antipolis
-
From: Yves Bertot <Yves.Bertot@sophia.inria.fr>
-
Date: Mon, 05 Jun 2000 15:54:32 +0200
-
Cc: "Pierre PARADINAS (E-mail)" <Pierre.PARADINAS@gemplus.com>, "Jean-louis LANET" <Jean-Louis.LANET@gemplus.com>
See the second part of this message for a translation in English.
Bourse de doctorat à l'INRIA Sophia Antipolis
Projet Lemme
le projet Lemme de l'INRIA Sophia Antipolis propose une bourse de
doctorat centrée sur les méthodes formelles basées sur Coq et sur la
description de langages de programmation adaptés aux cartes à puces.
Cette thèse s'intègrera dans le cadre d'une collaboration avec GemPlus,
entreprise à la pointe du développement des cartes à puces, Les
techniques étudiées devront permettre de développer des vérificateurs
de byte-code formellement certifiés pour des langages approximant le
langage JavaCard. L'objectif à terme est de fournir un vérificateur
de byte-code entièrement prouvé correct pour le langage JavaCard tel
qu'il est défini par JavaSun.
L'étudiant travaillant avec cette bourse doctorale aura l'occasion
d'approfondir ses compétences dans un domaine à l'intersection des
domaines théoriques les plus ambitieux de la logique et de
l'informatique fondamentale et des champs d'applications les plus
dynamiques de l'évolution récente des technologies de l'information et
de la communication (authentification, sécurité sur les réseaux,
commerce électronique...).
Les candidats intéressés devront envoyer un curriculum vitae et une
lettre de motivation à Yves Bertot (Yves.Bertot@sophia.inria.fr).
Liens utiles:
http://www-sop.inria.fr/lemme
http://www-sop.inria.fr/lemme/Yves.Bertot
http://www.gemplus.com
==================
In a collaboration with GemPlus, a leading company in the realm of
smartcards, the Lemme Project at INRIA Sophia Antipolis proposes a
PhD. grant centered around formal methods based on the Coq proof
system and the description of programming languages adapted to
smartcards. The studied techniques should make it possible to develop
formally certified bytecode verifiers for languages close to
JavaCard. The long term objective is to provide a fully formalized
bytecode verifier for the whole JavaCard language.
The student working on this topic will have the opportunity to
strengthen her or his competence in a domain at the frontier between
theoretical computer science and the most recent and exciting
evolution of information and communication technology.
Applications should be sent with a curriculum vitae to Yves Bertot
(Yves.Bertot@sophia.inria.fr).
For more web links:
http://www-sop.inria.fr/lemme
http://www-sop.inria.fr/lemme/Yves.Bertot
http://www.gemplus.com