Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Mon, 14 Feb 94 10:48:40 EST
From: "Thomas Kropf, Univ. Karlsruhe" <kropf@ira.uka.de>
To: info-hol@cs.uidaho.edu, isabelle-users@cl.cam.ac.uk, 
    theorem-provers@mc.lcs.mit.edu, lambda-usergroup@dcs.ed.ac.uk, 
    fg121@inferenzsysteme.informatik.th-darmstadt.de, 
    rewriting-list@lorraine.loria.fr, 
    deduktion@intellektik.informatik.th-darmstadt.de
Cc: nqthm-users@cli.com
Subject: CFP: Theorem provers in Circuit Design: TPCD94 (Reminder)
Message-Id: <"i80fs2.ira.303:14.01.94.09.48.56"@ira.uka.de>

This is a reminder for TPCD94's deadline, which is in about 5 weeks
(25 March 1994). 

TPCD94 will take place the week after 

 - The 7th International Workshop on Higher Order Logic Theorem Proving 
   and its Applications (Malta, 19-22 September)

 - EURO-DAC '94 (Grenoble, France, 19 - 23 September) and

 - The 3rd International School and Symposium in Real Time and Fault
   Tolerant Systems (Luebeck, Germany, 19 -23 September)

hence especially for people from outside Europe there is the opportunity 
to conveniently combine TPCD94 with one of the above events.

My apologies to all those who are on more than one of the above mailing
lists and got multiple copies of this reminder.

  --Thomas Kropf-- 

          +-------------------------------------------------------+
          |                                                       |
          |                   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 experi-
ments with new or established theorem proving tools, including tau-
tology 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 me-
thodologies, 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 exi-
sting tools and methodologies.

The intended audience includes workers in the field of hardware ve-
rification 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 Con-
ference 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.

BENCHMARK CIRCUITS

A set of benchmarks has been provided by anonymous ftp
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.

IMPORTANT DATES

The important dates are as follows:

25 March 1994:
	Final deadline for the submission of papers.
20 June 1994:
	Date for notification of acceptance.
8 July 1994:
	Final camera-ready copy due.
26-29 September 1994:
	Conference at Bad Herrenalb.

PROPOSALS FOR TUTORIALS

Proposals are solicited for tutorial presentations on relevant verifica-
tion 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 mathemati-
cal 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 presen-
tation. The proposals for tutorials will also undergo a review process
and it is proposed to have no more than 6 tutorials during the confe-
rence. Also welcome are proposals for demonstrations of working sy-
stems. Proposals for both tutorials and demonstrations should be sent
to the Tutorials Chair to arrive no later than 25 March 1994. The tuto-
rial papers will also be included in the proceedings.

PROGRAMME

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

ORGANIZATION

The conference is organized jointly by the Forschungszentrum Infor-
matik (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 and Benchmarks:
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)
David Dill (Stanford University, USA)
Hans Eveking (Univ. of Frankfurt, Germany)
Simon Finn (AHL, UK)
Mike Gordon (University of Cambridge, UK)
Keith Hanna (University of Kent, UK)
Warren A. Hunt Jr. (CL Inc. USA)
Paul Loewenstein (SUN, USA)
Miriam Leeser (Cornell Univ., USA)
Tom Melham (University of Glasgow, UK)
Tobias Nipkow (TU Muenchen, Germany)
David Shepherd (Inmos, UK)
Joergen Staunstrup (Lyngby Univ., Denmark)
Victoria Stavridou (Univ. of London, UK)
Pasupati Subrahmanyam (ATT Bell Labs, USA)

ADDRESSES FOR CORRESPONDENCE

The papers and all general correspondence should, in the first in-
stance, 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, Kaiserstr. 12, D-76128 Karlsruhe, Germany
email: kropf@informatik@uni-karlsruhe.de     FAX: +49 721 370 455
Tel.: +49 721 608 4220