Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Mon, 21 Nov 1994 00:06:44 +0000
Received: from localhost (listserv@localhost) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) id SAA13346 for qed-out;
          Sun, 20 Nov 1994 18:02:36 -0600
Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id SAA13341 
          for <qed@mcs.anl.gov>; Sun, 20 Nov 1994 18:02:30 -0600
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) 
          id RAA00365 for qed@mcs.anl.gov; Sun, 20 Nov 1994 17:06:06 -0700
Message-Id: <199411210006.RAA00365@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Sun, 20 Nov 1994 17:06:06 -0700
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: qed@mcs.anl.gov
Subject: Cohn paper on hardware verification
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Several people have asked for references.


@article{Cohn,
author={Avra Cohn },
title="The notion of proof in Hardware Verification",
journal="Journal of Automated Reasoning",
volume={5},
number={2},
year={1989},
page={127-140}
}

@incollection{Viper,
author={Avra Cohn },
title="A Proof of Correctness of the Viper Microprocessor: The First Level",
booktitle="VLSI Specification and Synthesis",
editor="Graham Birtwistle and P.A. Subrahmanyam",
publisher="Kluwer",
year={1988},
page={27-72}
}