Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Tue, 16 Nov 1993 11:26:49 -0800
From: coe@cs.uidaho.edu
Message-Id: <199311161926.AA11420@panther.cs.uidaho.edu>
To: tfm@dcs.gla.ac.uk
Cc: info-hol@cs.uidaho.edu, tfm@dcs.gla.ac.uk
In-Reply-To: <9311161323.AA02853@switha.dcs.gla.ac.uk>
Subject: Book Announcement.

tfm@dcs.gla.ac.uk writes:
 > 
 > 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.
 > 


How much of this book deals with the HOL theorem prover?


thanks  

mike
coe@cs.uidaho.edu