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; Mon, 18 Oct 1993 08:48:29 +0100
Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA16420;
          Mon, 18 Oct 93 01:37:23 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.4/16.2) id AA16414; Mon, 18 Oct 93 01:37:10 -0600
Received: from imec.be by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) 
          id AA23117; Mon, 18 Oct 93 00:36:36 -0700
Received: from imec.imec.be (imec) by imec.be (5.65c/IDA-1.4.4-IMEC) 
          id AA05143d; Mon, 18 Oct 1993 08:34:07 +0100
Date: Mon, 18 Oct 93 08:32:49 +0100
From: Catia Angelo <catia@imec.be>
Message-Id: <9310180732.AA25006@imec.imec.be>
Original-Received: by imec.imec.be Mon, 18 Oct 93 
                   08:32:49 +0100
PP-warning: Illegal Received field on preceding line
To: info-hol@cs.uidaho.edu
Subject: Re: Theorem provers of the world


The following are references on surveys and comparisons of formal systems:

@INPROCEEDINGS { Stav ,
        AUTHOR = "Stavridou, V. and Barringer, H. and Edwards, D.A." ,
        TITLE =  "``{Formal Specification and Verification of Hardware:
                  A Comparative Case Study}''" ,
        BOOKTITLE = "Proceedings of the 25th {ACM/IEEE} Design Automation
                     Conference" ,
        YEAR = "1988" ,
        PAGES = "197-203"
        }

@INPROCEEDINGS { Delta ,
        AUTHOR = "Levy, B." ,
        TITLE =  "``{An Overview of Hardware Verification Using the
                  State Delta Verification System}''" ,
        BOOKTITLE = "Proceedings of the {ACM/SIGDA}
          International Workshop in Formal Methods in {VLSI} Design" ,
        YEAR = "1991" ,
        ORGANIZATION = "Miami, FL" ,
        MONTH = "January"
        }

@ARTICLE { Wing ,
        AUTHOR = "Wing, J.M." ,
        TITLE = "``{A Specifier's Introduction to Formal Methods}''" ,
        JOURNAL = "IEEE Computer Magazine" ,
        YEAR = "1990" ,
        VOLUME = "23" ,
        NUMBER = "9" ,
        PAGES = "8-24" ,
        MONTH = "September" ,
        }

@ARTICLE { holbmart ,
        AUTHOR = "Angelo, C.M. and Verkest, D. and Claesen, L.
                 and {De Man}, H." ,
        TITLE = "``{On the Comparison of HOL and Boyer-Moore for Formal
                Hardware Verification}''" ,
        JOURNAL = "Formal Methods in System Design: An
                   International Journal" ,
        YEAR = "1993" ,
        VOLUME = "2" ,
        NUMBER = "1" ,
        PAGES = "45-72" ,
        MONTH = "February" ,
        NOTE = "Kluwer Academic Publishers"
        }

Regards,

Catia Angelo