Réunion du 20 Mars 2000


The first meeting was held on March 20th at INRIA Sophia-Antipolis.

Programme

10.30 Line Jakubiec (Oasis): Formalisation of the JCVM in Coq.

11.15 Yves Bertot (Lemme): Formalisation en Coq de la discipline de typage pour l'assembleur JVM concernant l'initialisation des objets

11.45 Pascal Brisset (France Telecom): A Case Study in Java Software Verification: Network Access Security

14.15 Jean Goubault (Coq): Presentation of Coq's research.

15.00 Thomas Jensen (Lande): Presentation of Lande's research.

16.00 Discussion.

Participants

A. Baala (Lemme), G. Barthe (Oasis), A. Bouali (Tick), Y. Bertot (Lemme), P. Brisset (France Telecom), D. Caromel (Oasis), F. Chalaux (Oasis), C. Courbis (Oasis), J. Despeyroux (Certilab), J. Goubault-Larrecq (Coq), B. Grégoire (Coq), L. Jakubiec (Oasis), T. Jensen (Lande), J.-L. Lanet (Gemplus), C. Loiseaux (Trusted Logic), E. Madelaine (RMI Sophia), D. Parigot (Oasis), L. Rideau (Lemme), M. Russo (Oasis), D. Sangiorgi (Mimosa), B. Serpette (Oasis), R. de Simone (Tick), S. Sousa (Oasis), B. Werner (Coq).
Back to the S-Java home page.
Gilles Barthe
Last modified: Mon Dec 4 10:03:40 MET 2000