The Coq mailing list

[Thomas Genet <genet AT irisa.fr>]

OPEN POSTDOCTORAL POSITION IN CERTIFIED ANALYSIS OF SOFTWARE 

A postdoctoral position is available, for one year, at IRISA,
Univ. Rennes 1, France. The position is connected to the Lande INRIA
project (http://www.irisa.fr/lande). The Lande project is concerned
with formal methods for constructing and validating software: testing,
static analysis by abstract interpretation, verification using proof
assistants and theorem provers.

In this group, we develop the verification tool called Timbuk
(http://www.irisa.fr/lande/genet/timbuk) which is based on rewriting,
tree automata and approximation techniques. We use Timbuk for
verifying cryptographic protocols. In this setting our tool produces a
tree automaton recognizing every possible behavior of a protocol
attacked by an intruder.

This postdoctoral position is concerned with developing and
certifying a program that checks that the produced tree
automaton is complete w.r.t. protocol and attacker capabilities
(described using term rewriting systems). Verification/certification
will be achieved using a proof assistant (Coq, PVS, Isabelle, ...).

A good knowledge and practice of program certification using a proof
assistant is necessary. Some knowledge in term rewriting and tree
automata would be also most useful.

If you are interested, send by e-mail (please, only ps or pdf files)
your resume including a list of publications, research statement with
three references to Thomas Genet 
(genet AT irisa.fr).
 



-- 
Thomas Genet - IFSIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44   E-mail: 
genet AT irisa.fr