Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 14 Jun 1994 22:02:11 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA06551;
          Tue, 14 Jun 1994 14:51:21 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA06546;
          Tue, 14 Jun 1994 14:51:19 -0600
Received: from ULTRASTAR.EE.CORNELL.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA14825;
          Tue, 14 Jun 1994 13:49:50 -0700
Date: Tue, 14 Jun 94 16:49:40 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Received: by ultrastar.EE.CORNELL.EDU (4.1/1.6.10+n-y-Cornell-Electrical-Engineering) 
          id AA09905; Tue, 14 Jun 94 16:49:40 EDT
Message-Id: <9406142049.AA09905@ultrastar.EE.CORNELL.EDU>
To: info-hol@cs.uidaho.edu
Subject: Information on uses of HOL for software verification



I am looking for information about uses of HOL for reasonably sized
software verification efforts.  A case study of HOL used to verify
software that is part of an actual software system is the kind of thing I
am looking for.  Any citations would be greatly appreciated.

Also, does anyone know of a good reference that discusses advantages
of higher-order logic theorem provers over first-order logic theorem
provers?

I need this information for the related work section of a journal
article I am working on.  One of the reviewers claimed that first
order logic is more familiar to people and fol systems are easier to
use.  I would like to present the "other side" of this argument.

Thanks for the help.

Miriam Leeser
mel@ee.cornell.edu