From owner-qed Sun Nov 20 18:04:28 1994 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 ; 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} }