FMPPTA'2002

Friday, April 19

8:45 - 9:00

Introduction
Michel Charpentier and Beverly Sanders

Session 1

9:00 - 9:30

From CSP-OZ to Java with Processes
Ana Cavalcanti and Augusto Sampaio

9:30 - 10:00

Proving a parallelisation criteria for multithreaded Java programs using the pi-calculus
Serge Chaumette and Pascal Grange

Coffee Break

Session 2

10:30 - 11:00

Formal Specification and Design of Mobile Systems
Gruia-Catalin Roman, Christine Julien and Qingfeng Huang

11:00 - 11:30

Composition and Refinement for Partial Object Specifications
Einar Broch Johnsen and Olaf Owe

11:30 - 12:00

Specification of an Access Control System with a Formalism Combining CCS and CASL
Gwen Salaun, Michel Allemand and Christian Attiogbe

Lunch Break

Session 3

1:30 - 2:00

Mechanical Verification of Hypercube Algorithms
Eric Gascard and Laurence Pierre

2:00 - 2:30

Proving self-stabilization with a proof assistant
Pierre Courtieu

2:30 - 3:00

Mixed Formal Specifications with PVS
Michel Allemand and Jean-Claude Royer

Coffee Break

Session 4

3:30 - 4:00

Program Composition in Isabelle/UNITY
Sidi O. Ehmety and Lawrence C. Paulson

4:00 - 4:30

An Approach to Compositional Model Checking
Hector Andrade and Beverly Sanders

4:30

Closing remarks and discussion

Michel Charpentier <>