
| IPDPS 1998 Workshop |
On the automatic validation of parameterized Unity programsProgram 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 1998Topics 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:
- Foundations of UNITY: proof theory, temporal logics
- Paradigms of concurrency and distribution in UNITY
- Case studies
- Refinement techniques and mapping
- Implementations of UNITY principles: theorem provers, environment, model checking techniques, etc.
- UNITY versus others frameworks: TLA, VDM, Z, B, RAISE, Action Systems, DISCO, CCS, PI calcul, OO, etc.
- Methods that extend or were motivated by UNITY
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: