ModoCop meeting

July 2nd, 2002

INRIA Rennes

salle Oléron, A008

Program

10.00 - 10.30	Gurvan Le Guernic (Lande) - Static Analysis of Java Programs with Threads
10.30 - 10.45	discussion
10.45 - 11.15	Rabéa Boulifa (Oasis) - Verification des propietes comportementales des programmes Java More information about this work can be found in Preuve de proprietes de comportement de programmes ProActive, INRIA Report RR-4460, by Rabéa Boulifa and Eric Madelaine, 2002.
11.15 - 11.30	discussion
11.30 - 12.00	Néstor Cataño (Lemme) - Event spaces, a formal semantics for concurrent Java
12.00 - 14.00	lunch
14.00 - 14.30	Frédéric Lang (Vasy) - NTIF
14.30 - 14.45	discussion
14.45 - 15.15	Moussa Amrani (Verimag) - Extracting IF models from Java
15.15 - 16.45	discussion

Some points for the discussion

a few financial and administrative remarks
common format: what has been observed so far about the different models, what is the way to proceed? What will be the goal of this topic? Understanding the different models and see how they are different or the same? Identify the maximal common subset between them?
how to extract finite state models from Java programs? What are the different approaches currently used? Bandera does something, Moussa will present an extraction, Nestors work could lead to another extraction method. What are the differences between these approaches? What are the commonalities?

If time permits, and people are interested Vlad Rusu could give an informal demo of Symbolic Test Generation and execution for smart cards.
Also, Marieke Huisman could say a few words about the logical channels in JavaCard 2.2 (my understanding of them, after reading the JavaCard 2.2 specifications).

Back to the ModoCop homepage.

Marieke Huisman

Last modified: Thu Jul 4 10:28:25 MEST 2002