The Coq mailing list

[jean-francois.monin AT imag.fr]

12 Months Postdoctoral Position at Verimag:
-------------------------------------------

Verimag is opening a post-doctoral research position on certification
of security properties for applications embedded on smart card.

The researcher will be integrated in the DCS team of Verimag, in a
research project that will start in March 2006.

Based on existing results, he will develop a rigorous and general
framework for certification of security properties following the
requirements of the Common Criteria (an International standard for
security evaluation). 

The aims of the project include:

- Certification of the result given by a model-checker by automatic
  generation of formal proofs which ensure that the checked 
  property holds.

- Formalization of the Common Criteria requirements : 
   security policies, refinement relation, correspondance between
   security properties and implementation mechanisms.

- Verification of properties by model-checking and abstraction


The former is the most challenging topic of this project. 

An important point is that all theoretical results are implemented in
prototype tools, and experimented in case studies provided by industrial
partners of the project. For this purpose, we want to use and further
develop recent results on model transformation techniques.


Please send your CV and motivation letter to
- Michaël Périn 
(michael.perin AT imag.fr)
or
- Marius Bozga  
(marius.bozga AT imag.fr)