The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

A postdoc position for 2 years is available at INRIA Rennes - Bretagne Atlantique.

The research will take place in the Celtique team (http://www.irisa.fr/celtique/). 

The task will consist in developing certificates of software which makes it possible 

for a user to check a downloaded code, in an automatic manner and extremely

quickly.  A program producer can hence verify the security of his program with a 

large amount of computation resource before distributing it with a certificate that 

helps the consumer to replay the verification program but with very far fewer resources. 

Candidates should have a background in program verification. Additional

knowledge in one or more of the following topics will be appreciated:

 - static analysis,

 - theory of abstract interpretation, 

 - language-based security,

 - deductive verification, 

 - proof assistant, 

 - decision procedures, 

 - probabilistic verification

 Knowledge of the French language is not required.

Start of contract: ideally, the candidate will start working in september or october, but

we can accomodate a later date.

Salaries: usual INRIA postdoc salary (2,357.30 euros gross/month, i.e. 1923,26 euros net/month).

Social security benefits:

  - Entitled to unemployment benefit at the end of the contract;

  - Affiliated to the French social security system.

Candidates should submit to david.pichardie[at]irisa.fr 

  - A CV including a list of publications

  - A one-page research statement

  - Referee reports for the PhD thesis if any

  - Contact information for two references (including the PhD supervisor)