Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <21301-0@swan.cl.cam.ac.uk>; Thu, 31 Oct 1991 23:44:07 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA06461;
          Thu, 31 Oct 91 15:35:49 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (15.11/1.34)
          id AA06457; Thu, 31 Oct 91 15:35:45 pst
Received: from localhost by panther.cs.uidaho.edu with SMTP
          id AA05153 (5.65c/IDA-1.4.4 for info-hol@ted);
          Thu, 31 Oct 1991 15:38:35 -0800
Message-Id: <199110312338.AA05153@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: EUARTSD Workshop Announcement; please redistribute as appropriate
Date: Thu, 31 Oct 91 15:38:34 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>
X-Mts: smtp


***********************************************************************
*                         CALL FOR PAPERS                             *
*                                                                     *
*                        Workshop on the                              *
*        Effective Use of Automated Reasoning Technology in           *
*                       System Development                            *
*                                                                     *
*                                                                     *
*                       April 6-8, 1992,                              *
*             Naval Research Laboratory, Washington, D.C.             *
***********************************************************************

Mathematics and logic are fundamental tools needed to construct complex
computer-based systems that must satisfy critical requirements (e.g.,
for safety and security).  Work in formal methods, particularly in
specification techniques, is increasing our ability to apply these
tools where they are needed.  Once a system is formally specified, it
becomes possible to check rigorously whether the specification has
certain (also formally specified) properties desired of it.  Technology
to support reasoning about formal specifications, including automated
theorem provers and other analysis tools, has been developing in
parallel with formal specification methods.  At present, a particular
formal specification technique is typically tied to a specific
automated theorem prover, and one must choose in advance, based on the
kinds of theorems one intends to prove about a system, which formal
specification language and theorem prover to use.

The purpose of this workshop is to explore issues in the application of
automated reasoning technology to systems with critical requirements, to
investigate how different automated tools might be brought to bear on a
single system specification, and to consider how future automated tools
might be organized to promote greater interchangeability of component
parts.

The workshop is sponsored by the Technical Panel on Trustworthy
Computing Technology (XTP-1) under The Technical Cooperation Program
(TTCP), an agreement under which the US, UK, Canada, Australia, and New
Zealand share defense research and development information.

Attendance will be limited to 40 individuals and is by invitation on
the basis of a submitted paper, extended abstract, or position
statement. Copies of all accepted papers will be mailed to participants
prior to the workshop and will be published subsequently in a publicly
available TTCP report.


Important dates:
   January 10, 1992:  Submissions due at the address listed below.
   February 7, 1992:  Acceptances and invitations to participate mailed;
                     (Information for authors regarding paper format
                      to be provided at this time.)
   March 6, 1992:    Camera-ready copies of papers due.
   April 6-8, 1992:  Workshop held



[More information on reverse side]


Location and Date:

The workshop will be held at the Naval Research Laboratory,
Washington, D.C. April 6-8, 1992.

Areas of Interest:

1.  Application of different automated reasoning tools to the same problem
    or specification.
2.  Methods for exchanging useful data among automated theorem provers,
    software engineering tools, and other analysis tools.
3.  Methods for promoting the interchangeability of component parts of
    automated reasoning tools.
4.  Establishing a formal basis for exchanging information among automated
    reasoning tools and between formal specification processing tools and
    automated theorem provers.
5.  The effectiveness of alternative user interfaces and interaction styles
    for automated reasoning tools.
6.  Significant applications of automated reasoning technology to system
    development.

Organizing Committee:

Carl Landwehr, Naval Research Laboratory, USA, Chair
C. Terrence Ireland, NSA, USA
Milan Kuchta, Canadian Systems Security Centre, Canada
William Scherlis,  DARPA, USA


Please send inquiries and (FOUR COPIES OF) your proposed workshop
contributions to:

Carl E. Landwehr
XTP-1 Workshop
Code 5542
Naval Research Laboratory,
Washington, D.C. 20375-5000

Phone:    +1(202)767-3381
Fax:      +1(202)404-7942
Internet: landwehr@itd.nrl.navy.mil

****************************************************************************


------- End of Forwarded Message


