Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Message-Id: <9307151538.AA06514@cs.uidaho.edu>
To: John.Herbert@cl.cam.ac.uk, jmch@mimosa.unice.fr, jluc@gyptis.univ-mrs.fr, 
    jli@dione.hut.fi, jifeng@comlab.ox.ac.uk, jess@es.ele.tue.nl, 
    jan@vlsi.cs.caltech.edu, jam@minster.york.ac.uk, jackson@cs.cornell.edu, 
    jack@dcs.gla.ac.uk, info-hol@cs.uidaho.edu, 
    indermark@informatik.rwth-aachen.de, hwcomp@prg.ox.ac.uk, 
    howden@cs.ucsd.edu, howard@r3.cs.man.ac.uk, horning@src.dec.com, 
    holger%sun11b@ztivax.zfe.siemens.de, hoare@prg.ox.ac.uk, hill@hermes.mod.uk, 
    hhl@id.dth.dk, helen@mimosa.unice.fr, hearn@rand.org, Han.Yan@prg.ox.ac.uk, 
    haehnle@ira.uka.de, gwinskel@daimi.aau.dk, gthuau@imag.fr, 
    grass@acrux.fmi.uni-passau.de, Grant.Malcolm@prg.ox.ac.uk, 
    graham@r3.cs.man.uk, graham@cpsc.ucalgary.ca, good@cli.com
Subject: TPCD94 Call for PApers
Date: Thu, 15 Jul 93 17:25:02 MET DST
From: kropf@ira.uka.de


A (nicer) Postscript version of the call can be found at the anonymous 
ftp-server goethe.ira.uka.de (129.13.18.22) in the directory /pub/tpcd94.


          +-------------------------------------------------------+
          |                                                       |
          |                   CALL FOR PAPERS                     |
          |                                                       |
          |         Second International Conference on            |
          |                                                       |
          |         THEOREM PROVERS IN CIRCUIT DESIGN:            |
          |          Theory, Practice and Experience              |
          |                                                       |
          |        Bad Herrenalb (Blackforest), Germany           |
          |             26. - 29. September 1994                  |
          |                                                       |
          |         In cooperation with  IFIP WG 10.2             |
          |                                                       |
          +-------------------------------------------------------+

FOCUS AND OBJECTIVES
====================

The use of formal methods in the design of digital systems is steadily
gaining popularity.
The  practicability of such techniques, however, depends on the support
of appropriate mechanized verification tools.  

This conference is a sequel to the one held at Nijmegen in June 1992,
and provides a forum for discussing the role of theorem provers in the
design of digital systems.  The objective is to cover all relevant 
aspects of work in the field, i.e. verification, synthesis and testing, 
including original research as well as case studies and other practical 
experiments with new or established theorem proving tools, including 
tautology and model checkers.  

The primary focus will be on the ways in which formal methods can be
incorporated into hardware design tools and hardware design methodologies, 
rather than the theory underlying the theorem provers. 
Topics of interest include the philosophy behind the incorporation of 
formal techniques in design tools, hardware specification languages, 
the design and development and evaluation of formally-based  tools, and 
the integration of formally based design and verification with existing 
tools and methodologies. 

The intended audience includes workers in the field of hardware
verification as well as practising digital designers with little or no
prior knowledge in formal methods. 

SUBMITTING A PAPER
==================

Five copies of a complete paper (in English) should be sent to the 
Conference Chair at the address given below to arrive no later than 
25 March 1994.  Electronic mail submissions in a postscript format
are also acceptable.
Papers must not exceed 6000 words in length, with full-page figures
counted as 300 words.  Each paper should include a 300 word abstract.  
All papers will be refereed and the final choice will be made by the 
programme committee on the grounds of relevance, significance, originality, 
correctness, clarity and the use of given benchmark circuits (see below).  

The conference proceedings will be published by a major publisher.

PROPOSALS FOR TUTORIALS
=======================

Proposals are solicited for tutorial presentations on relevant verification 
tools and provers. The intention is that a tutorial will provide an overview 
of the basic ideas behind the tool using a completely worked out example, 
rather than a detailed instruction on how to use it, hence the use of 
benchmark circuits is also suggested.  
The tutorials should include an assessment of strengths and weaknesses  
of the tools and should concentrate on general issues such as security, 
robustness, the degree of interaction required, the user interface, and the 
mathematical skill required of the user.  

Proposals for tutorials should not exceed 6000 words in length and should 
give a clear indication of the topic and structure of the presentation.
The proposals for tutorials will also undergo a review process and it is
proposed to have no more than 6 tutorials during the conference.
Also welcome are proposals for demonstrations of working systems.
Proposals for both tutorials and demonstrations should be sent to the 
Tutorials Chair to arrive no later than 25 March 1994.
The tutorial papers will also be included in the proceedings.

BENCHMARK CIRCUITS
==================

A set of benchmarks will be provided by anonymous ftp after 3 December
1993 at goethe.ira.uka.de (129.13.18.22). The circuits as well as
detailed instructions on how to use them can be found in the directory 
/pub/tpcd94/benchmarks. 

All authors submitting a regular paper or a proposal for a tutorial are 
strongly encouraged to make use of these circuits. 

PROGRAMME
=========

The conference programme will start with a day of tutorials and is followed 
by three days of presentations by contributing authors. The late afternoon 
sessions will be reserved for demonstrations. 
The programme will also include invited lectures by prominent researchers 
in the field of machine-assisted verification. The names of the invited
speakers will be announced in due course.

IMPORTANT DATES
===============

The important dates are as follows.

 3 December 1993:
       Benchmarks available via anonymous ftp.
 25 March 1994:
       Final deadline for the submission of papers.
 3 June 1994:
       Date for notification of acceptance.
 1 July 1994:
	Final camera-ready copy due.
 26-29 September 1994:
	Conference at Karlsruhe.

ORGANIZATION
============

The conference is organized jointly by the Forschungszentrum Informatik (FZI), 
Karlsruhe and the Institute of Computer Design and Fault Tolerance at the 
University of Karlsruhe, Germany.

The conference organizers are:

Conference Chair:   Ramayya Kumar, FZI Karlsruhe
Programme Chair:    Mike Fourman, Edinburgh University
Tutorials Chair:    Thomas Kropf, University of Karlsruhe
Local Arrangements: Hilke Kloss, FZI Karlsruhe


PROGRAMME COMMITTEE
===================
 
 Dominique Borrione (IMAG, France) 
 Holger Busch (Siemens AG, Germany) 
 Luc Claesen (IMEC, Belgium) 
 D. Dill (Stanford University, USA) 
 Hans Eveking (Univ. of Frankfurt, Germany)
 Simon Finn (AHL, UK) 
 Mike Gordon (Univ. of Cambridge, UK) 
 Keith Hanna (Univ. of Kent, UK) 
 Warren A. Hunt Jr. (CL Inc. USA) 
 Paul Loewenstein (SUN, USA) 
 Miriam Leeser (Cornell Univ., USA) 
 Tom Melham (Univ. of Cambridge, UK) 
 Tobias Nipkow (TU Muenchen, Germany)
 David Shepherd (Inmos, UK)
 Jorgen Staunstrup (Lyngby Univ., Denmark)
 Victoria Stavridou (University of London, UK)
 Pasupati Subrahmanyam (ATT Bell Labs, USA)


ADRESSES FOR CORRESPONDANCE
===========================

The papers and all general correspondence should, in the first instance, 
be sent to the Conference Chair:

Ramayya Kumar
TPCD Conference Chair
Forschungszentrum Informatik
Department - ACID
Haid-und-Neu Strasse 10-14 
76131 Karlsruhe, Germany
Tel: (+49) 721 9654-419 
Fax: (+49) 721 9654-459
Email: kumar@fzi.de


Proposals for tutorials, demonstrations and everything related to the 
benchmark circuits should be sent to the Tutorials Chair:

Thomas Kropf
TPCD Tutorials Chair
Universitaet Karlsruhe
Inst. f. Rechnerentwurf u. Fehlertoleranz
P.O. Box 6980
76128 Karlsruhe, Germany
Tel: (+49) 721 608-4220 
Fax: (+49) 721 370 455
Email: kropf@ira.uka.de

All correspondence should include a return postal address and, if possible, 
Fax and email address.

-- 
Thomas Kropf, Institut fuer Rechnerentwurf und Fehlertoleranz,
Universitaet Karlsruhe, P.O. Box 6980, D-76128 Karlsruhe, Germany
email: kropf@ira.uka.de     Tel.: +49 721 608 4220    FAX: +49 721 370 455