Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9311161323.AA02853@switha.dcs.gla.ac.uk>
To: info-hol@cs.uidaho.edu
Cc: tfm@dcs.gla.ac.uk
Subject: Book Announcement.
Date: Tue, 16 Nov 93 13:23:05 +0000


The attached publisher's mailshot may be of interest to readers of
info-hol involved with teaching and research in hardware verification.

Tom

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

   Higher Order Logic and Hardware Verification

   T. F. Melham

   Cambridge Tracts in Theoretical Computer Science 31
   Cambridge University Press, 1993.
   176pp, hardback.  ISBN 0-521-41718-X
   UK list price: 24.95 pounds net.

   Blurb: 

   Dr Melham shows here how formal logic can be used specify the
   behaviour of hardware designs and reason about their correctness.
   A primary theme of the book is the use of abstraction in hardware
   specification and verification. The author describes how certain 
   fundamental abstraction mechanisms for hardware verification can
   be formalised in logic and used to express assertions about design
   correctness and the relative accuracy of models of hardware behaviour.

   His approach is pragmatic and driven by examples.  He also includes
   an introduction to higher order logic, which is a widely used formalism 
   in this subject, and describes how that formalism is actually used for
   hardware verification.

   This book is based in part on the author's own research, as well as
   on graduate teaching.  This it can be used to accompany courses on
   hardware verification and as a resource for research workers.