The Coq mailing list

[sorin stratulat <stratulat AT univ-metz.fr>]

[[[ Apologies for multiple copies of this message ]]]

---------------------------------------------------------------------
|                                                                   |
|                    Ph.D. Position Available on                    |
|                                                                   |
|         Formal Verification in Telecommunications Systems         |
|                                                                   |
|                     proposed by France Telecom R&D                |   
|           and LITA -- University Paul Verlaine of Metz,           |
|                                France                             |
|                                                                   |
|                   Firm deadline: September 28th, 2005.            |
|                                                                   |
---------------------------------------------------------------------

France Telecom R&D and LITA (Laboratoire de l'Informatique Theorique
et Appliquee) is seeking a candidate for a Ph.D. position at the
University Paul Verlaine of Metz, France.

The work will be carried out within the France Telecom R&D and
LITA laboratories and mainly consists in the design and development of
automatic proving techniques and tools for formally verifying critical
telecommunications applications, like the management of security
policies.


Presentation
============

Candidates should introduce themselves by sending email to:

                    
stratulat AT univ-metz.fr

Please use 'PHD CANDIDATE' as subject, and include a statement of
interest and a CV. PostScript, PDF, or plain text formats are
encouraged.


Candidate Profile
=================

The ideal candidate should have a MS equivalent (in either computer
science or mathematics), and combine solid theoretical background and
software development skills.

Background knowledge and/or previous experience in the areas of formal
verification and strong programming skills using functional languages
(like Ocaml) and Java, though not mandatory, will be considered
favourably. Also, any experience with building Eclipse plugins and
applications is a plus.

The candidate should be able to work in a collaborative environment,
with a strong commitment to achieving assigned objectives and reaching
research excellence.


Work Description
================

Spike is an automated induction-based theorem prover currently
developed at the University Paul Verlaine of Metz that was
successfully used in the validation of critical software, like
telecommunications protocols [1] and JavaCard bytecode [2]. It is able
to prove inductive theorems in models specified by sets of conditional
rewrite rules. Such formalisms are adequate for telecommunications
domains concerning the cryptographic protocols and the security
policies. The main goal is to develop a theory and a Spike-like tool
able to verify that a security policy satisfies some context properties. 

The theoretical part consists in finding solutions for integrating and
extending different security policy aspects within the tool. It may
concern implicit induction and proof-by-saturation techniques to deal
with "workflow" properties, and decision procedures to automatize the
reasoning on (sub)theories of interest: sets, ordered sets,
arithmetics, etc. The candidate should master the domain of security
policies and match it with the logic of the tool by taking into
account their modularity conditions and the potential abstractions.


[1] M. Rusinowitch, S. Stratulat and  F. Klay. Mechanical verification
of   an  ideal incremental  ABR    conformance  algorithm. Journal  of
Automated Reasoning, 30(2): 153--177, 2003


[2] G. Barthe  and S. Stratulat.  Validation of  the JavaCard Platform
with   Implicit   Induction   Techniques. In   Proceedings  of    14th
International  Conference   on Rewriting Techniques  and  Applications
(RTA'2003). Springer Verlag, 2003.



Payment
=======

The candidate is expected to finish the PhD after three years. During
the first two years, the salary is about 1600 euros/month, and 1800
euros/month during the third year.


Contact Person
==============

Sorin Stratulat 
mailto:stratulat AT univ-metz.fr
http://www.lita.sciences.univ-metz.fr/~stratula