Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl, victoria@uk.ac.rhbnc.cs
Subject: Another book announcement.
Date: Tue, 18 Aug 92 16:39:11 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.052:18.07.92.15.42.18"@cl.cam.ac.uk>


The following publisher's mailshot may also be of interest to
readers of info-hol.

Perhaps someone could post similar information for proceedings
of last years HOL user meeting?

Tom

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

   Theorem Provers in Circuit Design

   Proceedings of the IFIP WG10.2 International Conference
   on Theorem Provers in Circuit Design: Theory, Practice,
   and Experience, Nijmegen, The Netherlands, 22-24 June 1992.

   Edited by V. Stavridou, T. F. Melham and R. T. Boute

   1992 xii+360 pages, paperback.  

   Price: US $108.50/Dfl. 190.00 [The Dutch price is definitive]
   ISBN 0-444-89686-4
   Included in IFIP Transactions A

   The papers in this volume address the role of mechanized theorem
   proving technology in the design of digital systems.  The primary
   focus is on the practical application of theorem provers to digital
   design, rather than on theoretical foundations.  The diverse
   contributions include invited papers by the leading researchers
   Gordon and Hunt, as well as technical contributions by many other
   prominent researchers in the field of machine-assisted hardware
   verification.  This side of the Proceedings reflects current 
   research activity, and the section containing tutorial papers
   on several influential theorem provers serves as an introduction
   to this exciting field.

   Contents. RESEARCH PAPERS.  Invited paper: Introduction to a
   Formally Defined Hardware Description Language (B.C. Brock,
   W.A. Hunt, Jr. and W.D.  Young).  A Description Methodology for
   Parameterized Modules in the Boyer-Moore Logic (D. Verkest, J.
   Vandenbergh, L. Claesen and H. De Man).  Hierarchical
   Mixed-mode Verification of Complex FSMs Described at the RT
   Level (T. Margaria).  Implementation of the Veritas Design
   Logic (K. Hanna, N. Daeche and G. Howells).  Synchronous
   Realization of Asynchronous Computations (H.H. Lovengreen and
   J. Staunstrup).  Modelling and Verification of Timing
   Conditions with the Boyer Moore Prover (D.J. Kinniment and A.M.
   Koelmans).  Invited paper: Experience with Embedding Hardware
   Description Languages in HOL (R. Boulton, A. Gordon, M. Gordon,
   J. Harrison, J. Herbert and J. Van Tassel).  Incremental Design
   and Formal Verification of Microcoded Microprocessors (J.M.J.
   Herbert).  Transformational Design in a Theorem Prover (H.
   Busch).  FUNNEL and 2OBJ: Towards an Integrated Hardware Design
   Environment (V.  Stavridou, J.A. Goguen, A. Stevens, S.M. Eker,
   S.N. Aloneftis and K.M. Hobley).  Verification of a
   Fault-Tolerant Property of a Multiprocessor System: A Case
   Study in Theorem Prover-Based Verification (M. Bickford and M.
   Srivas).  Theorem Proving as an Industrial Tool for System
   Level Design (S. Bainbridge, A.  Camilleri and R. Fleming).
   TUTORIAL PAPERS.  Mechanized Verification of Circuit
   Descriptions using the Larch Prover (J.  Staunstrup, S.J.
   Garland and J.V. Guttag).  The Veritas Design Logic: A User's
   View (K. Hanna and N. Daeche).  Nuprl and its Use in Circuit
   Design (P.B.  Jackson).  Using the State Delta Verification
   System (SDVS) for Hardware Verification (B. Levy, I. Filippenko, 
   L. Marcus and T. Menas).

   Orders: Elsevier Science Publishers, P.O. Box 211, 1000 AE
   Amsterdam, The Netherlands.
   
   U.S. and Canada: Elsevier Science Publishers Co, Inc.,
   P.O. Box 945, Madison Square Station, New York, NY 10160-0757.

   Orders from indivuals must be accompanied by a remittance,
   following which books will be supplied postfree.