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; Mon, 5 Jun 1995 20:36:24 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA192969049; Mon, 5 Jun 1995 13:04:09 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from gateway.sctc.com by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA192869034; Mon, 5 Jun 1995 13:03:54 -0600 Received: from sccmailhost.sctc.com (sccmailhost.sctc.com [192.55.214.100]) by gateway.sctc.com (8.6.10/8.6.9) with SMTP id OAA13378 for ; Mon, 5 Jun 1995 14:05:08 -0500 Received: from sccmailhost.sctc.com by sccmailhost.sctc.com id 080750000; 5 Jun 95 15:04 CDT Received: from sctc.com by sccmailhost.sctc.com id 208300000; 5 Jun 95 15:04 CDT Received: from arcadia.sctc.com (arcadia.sctc.com [172.17.192.112]) by spirit.sctc.com (8.6.12/8.6.9) with ESMTP id NAA06930 for ; Mon, 5 Jun 1995 13:58:14 -0500 Received: (from coe@localhost) by arcadia.sctc.com (8.6.12/8.6.9) id OAA03660; Mon, 5 Jun 1995 14:03:28 -0500 Date: Mon, 5 Jun 1995 14:03:28 -0500 From: Mike Coe Message-Id: <199506051903.OAA03660@arcadia.sctc.com> To: info-hol@leopard.cs.byu.edu Subject: software spec Organization: Secure Computing Corp. X-Zippy: Mr and Mrs PED, can I borrow 26.7% of the RAYON TEXTILE production Hello, while there are numerous examples of hardware specification and verification in HOL, I know of little in the area of software specification. since I have not been following HOL to closely for about a year now, could someone point to some good examples of this. In case anyone is wondering, my company is about to make a major decision about what formal spec language to use for a project. we want theorem prover support, but it is not mandatory. any help is appreciated, mike coe@sctc.com