Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id NAA13098; Wed, 11 Oct 1995 13:44:09 +0200
Message-Id: <199510111144.NAA13098@ra.abo.fi>
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA120056792; Wed, 11 Oct 1995 04:19:52 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA120026783; Wed, 11 Oct 1995 04:19:43 -0600
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk 
          with LOCAL SMTP (PP); Wed, 11 Oct 1995 11:11:13 +0100
To: info-hol@leopard.cs.byu.edu
Cc: tfm@dcs.gla.ac.uk
Subject: CFP relevant to HOL users.
Date: Wed, 11 Oct 1995 11:11:09 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>

Note that this call mentions theorem-prover based work.
Tom
=====================================================================
                           SECOND CALL FOR PAPERS
			      FMPPTA'96

		      International Workshop on
  Formal methods for parallel programming:  theory and applications
		    to be held in conjunction with
      10th International Parallel Processing Symposium IPPS'96}
			  April 15-19, 1996
	      Sheraton Waikiki Hotel,  Honolulu, Hawaii
			     Sponsored by
IEEE Technical Computer Society Technical Committee on Parallel Processing
		   in cooperation with ACM SIGARCH




The workshop  is held,  during   one full-day  (April 15,  1996),   in
conjunction  with  10th  International   Parallel Processing Symposium
IPPS'96.  The workshop will be held as  part of IPPS'96 and there will
not be separate registration for the workshop.

				TOPICS



Formal  methods are widely investigated  in academic institutions and,
more recently, used  in industrial applications. By using mathematical
notations, systems and  their properties are precisely  described, and
therefore  formal methods offer a way  to achieve high level assurance
of system quality.  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 objectives of the workshop is
to gather together 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 formalisation of the parallel programming process.

Papers are invited in areas such as (but not limited to) the following:




o Methodological and theoretical aspects of parallel programming with
respect to the development of parallel programs: specification,
verification, refinement, compositionality, correctness, abstract
interpretation, transformation, translation...

o Case studies developed with formal methods, particularly those with
industrial background.

o Tools  that  support formal development of parallel programs, with
emphasis on re-use and modularisation.  

o Examples of existing formal languages (for example, RAISE, UNITY, B,
VDM, Z, SWARM, GAMMA, PVS, TLA, ISABELLE ...) and their application to
parallel program problems.

o Comparative studies of existing formal methods for parallel
programming



=========================
= PRACTICAL INFORMATION =
=========================


Program Chair: Dominique M\'ery (Universite Henri
Poincare,Nancy,France) 


Program Committee:
=================

Radhia Cousot (CNRS  & Ecole Polytechnique, France)
Pascal Gribomont, (Li\`ege,  Belgium)
Silvio Lemos Meira, (Recife, Brazil)
Dominique M\'ery, (Nancy, France  (Chair))
Lawrence Paulson, (Cambridge , UK)
Xu Qiwen, ( Macau)
Catalin Roman, (St Louis,  USA)


IMPORTANT DATES

Deadline for submissions:            November 15, 1995
Notification of acceptance/rejection:December   31, 1995
Deadline for final text:             January  31, 1995
Workshop:                            April 15, 1996
IPPS'96 :                            April 15--19, 1996



SUBMISSIONS

To submit an original research paper, send the workshop chair 4 hard
copies of your complete manuscript (not to exceed 20 double-spaced
pages of text including references, figures, tables, etc. and using 12
point type on 8.5 x 11 inch pages).  Please include your postal
address, e-mail address, telephone and fax numbers.  All manuscripts
will be reviewed.  Manuscripts must be received by November 15, 1995
(Email submission is accepted as a PostScript file or a Latex file).
Notification of review decisions will be mailed by December 31, 1995.
Camera-ready papers are due January 31, 1996.  Proceedings will be
available at the Symposium and via WWW.


INFORMATION

email:mery@loria.fr
or 
WWW:http://www.usc.edu/dept/ceng/prasanna/meetings/ipps/ipps96/ippshome.html 
or surface mail: 
FMPPTA'96/Dominique M\'ery 
Universit\'e Henri Poncare\'e-Nancy 1, 
CRIN-CNRS \& INRIA Lorraine, 
Batiment LORIA, BP239 
F-54506 Vand\oe uvre-l\`es-Nancy France 
Phone: +33 83 59 20 14  
Fax: +33 83 41 30 79 
WWW:http://www.loria.fr/~mery/


=====================================================================
