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; Wed, 1 Mar 1995 14:28:56 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA213856520; Wed, 1 Mar 1995 07:02:00 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from electra.cc.umanitoba.ca by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA213826516; Wed, 1 Mar 1995 07:01:57 -0700 Received: from canopus.cc.umanitoba.ca (root@canopus.cc.umanitoba.ca [130.179.16.24]) by electra.cc.umanitoba.ca (8.6.10/8.6.9) with ESMTP id IAA29382 for ; Wed, 1 Mar 1995 08:00:50 -0600 From: rahard@ee.UManitoba.CA Received: from eeserv.ee.UManitoba.CA (root@eeserv.ee.umanitoba.ca [130.179.8.1]) by canopus.cc.umanitoba.ca (8.6.10/8.6.9) with SMTP id IAA25202 for ; Wed, 1 Mar 1995 08:00:45 -0600 Received: from ic14.ee.umanitoba.ca by eeserv.ee.UManitoba.CA (4.1/25a-eef) id AA21955; Wed, 1 Mar 95 08:00:44 CST Received: by ic14.ee.umanitoba.ca (4.1/25-eef) id AA27355; Wed, 1 Mar 95 08:00:43 CST Message-Id: <9503011400.AA27355@ic14.ee.umanitoba.ca> Subject: Mechanizing CSP To: info-hol@leopard.cs.byu.edu Date: Wed, 1 Mar 1995 08:00:43 -0600 (CST) X-Mailer: ELM [version 2.4 PL22] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 740 I am reading A.J. Camilleri, "Mechanizing CSP Trace Theory in Higher Order Logic," IEEE Trans. on Software Eng., vol 16, no. 9, pp. 993--1004, Sept 1990. Is there a package/theory available for this? Is there related/newer HOL references/package/theory related to CSP? I am also looking for software/environment to manipulate/execute/ model checking CSP. From the Formal Methods home page : http://www.comlab.ox.ac.uk/archive/formal-methods.html there are two tools: FDRtool and CCSP. Any comments about these tools? Anything I should know before grabbing them? thanks -- budi -- Budi Rahardjo Electrical and Computer Engineering - University of Manitoba - Canada