Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 27 Jan 1995 18:55:44 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA04303; Fri, 27 Jan 1995 11:33:27 -0700 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.38.193.4/16.2) id AA04298; Fri, 27 Jan 1995 11:33:26 -0700 Received: from crl.dec.com (crl.dec.com [192.58.206.2]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id KAA09988 for ; Fri, 27 Jan 1995 10:31:45 -0800 Received: by crl.dec.com; id AA17265; Fri, 27 Jan 95 13:29:00 -0500 Received: by easynet.crl.dec.com; id AA22596; Fri, 27 Jan 95 13:20:13 -0500 Message-Id: <9501271820.AA22596@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Fri, 27 Jan 95 13:28:59 EST Date: Fri, 27 Jan 95 13:28:59 EST From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@cs.uidaho.edu Cc: leonard@ricks.enet.dec.com Apparently-To: info-hol@cs.uidaho.edu Subject: Science article This week's issue of Science (20 January 1995, pp332-333) has an article about formal verification, using the Pentium bug to illustrate the need. Though it mentions interactive theorem proving, the emphasis is on model checking, and BDD-based methods. It includes the textual equivalent of sound bites from Pixley, Kurshan, Rushby, Boyer, Clarke, Bryant, Dill, and others.