Third International Workshop on Formal
Methods for Parallel Programming:
Theory & Applications (FMPPTA '98)

IPDPS 1998 Workshop

Program and Organizing Chair's Message:

It is our pleasure to welcome you to the Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications, FMPPTA'98. This message pays tribute to the many people who have contributed their time and effort in organizing this meeting and reviewing papers.
We are thankful to the IPPS'98 committee for accepting the organization of the workshop in cooperation with IPPS'98, and especially Viktor K. Prasanna and Jose Rolim.
We also would like to thank the authors of all submitted papers, the presenters of accepted papers, the session chairs, the invited speakers and the program committee members.
We hope that every participant will enjoy the workshop.

Beverly Sanders and Dominique Mery
January 1998

Topics of the workshop:

Formal methods have been widely investigated in academic institutions. More recently they are being applied in industry. Systems and their properties can be described precisely using mathematical notations, offering a way to achieve higher reliability. Formal methods combine methodological aspects in a formal framework. Although they appear to be difficult to apply, they are the only means of ensuring that an implementation is correct with respect to a given specification. The development of an algorithmic solution from a (formal) specification is carried out with the help of mathematical techniques and tools. The objective of the workshop is to gather people, both from academia and industry, who use and/or develop formal methods for parallel programming. There are potentially many different approaches to improving the environment for parallel programming. The (proof) tools and their user interface are fundamental to formalization of the parallel programming process. Since 1998 marks the 10th anniversary of UNITY, we have especially encouraged UNITY related work including:

We are also pleased to announce that UNITY inventors K. Mani Chandy (Caltech) and Jayadev Misra (U Texas, Austin) have both agreed to speak at FMPPTA'98.

Program Committee:

Flemming Andersen (Tele Danmark R&D, Denmark), Mani Chandy (Caltech, USA), Radhia Cousot (CNRS & Ecole Polytechnique, France), Pascal Gribomont (Liege, Belgium), Dominique Mery (LORIA, Universite Henri Poincare and Institut Universitaire de France, Nancy France (CoChair)), Lawrence Paulson (Cambridge, UK), Xu Qiwen (Macau), Catalin Roman (St Louis, USA), Beverly Sanders (University of Florida (CoChair), USA), Ambuj Singh (University of California at Santa Barbara, USA) Mark Staskauskas (Bell Laboratories, Lucent Technologies, USA)


Program:

On the automatic validation of parameterized Unity programs
J.-P. Bodeveix, M. Filali

A cottage industry of sofware publishing: implications for theories of composition
K. M. Chandy, P. A. G . Sivilotti, J. R. Kiniry

Tailoring UNITY to distributed program design
M. Charpentier, M. Filali, P. Mauran, G. Padiou, P. Queinnec

Mechanically verifying the correctness of the fast Fourier transform in ACL2
R. A. Gamboa.

Experiments with program parallelization using archetypes and stepwise refinement
B. L. Massingill.

An object model for multiprogramming
J. Misra

Deriving efficient cache coherence protocols through refinement
R. Nalumasu, G. Gopalakrishnan

Building BSP programs using the refinement calculus
D. B. Skillicorn

An introduction to mobile UNITY
G.-C. Roman, P. J. McCann

Automatically proving UNITY safety properties with arrays and quantifiers
X. Thirioux.