Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from toadflax.cs.ucdavis.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <26319-0@swan.cl.cam.ac.uk>; Mon, 20 Jan 1992 16:24:56 +0000
Received: from motgate.mot.com by toadflax.cs.ucdavis.edu (4.1/UCD.CS.1.0)
          id AA05270; Mon, 20 Jan 92 08:09:27 PST
Received: from pobox.mot.com ([129.188.137.100])
          by motgate.mot.com (4.0/SMI-4.0) id AA17802;
          Mon, 20 Jan 92 10:09:46 CST
Received: from cadsun.corp.mot.com ([129.188.128.6])
          by pobox.mot.com (4.1/SMI-4.0) id AA18706;
          Mon, 20 Jan 92 10:09:39 CST
From: ramu@com.mot.corp.cadsun
Received: from munich.srd.mot by cadsun.corp.mot.com (4.0/SMI-4.0) id AA17227;
          Mon, 20 Jan 92 10:06:56 CST
Date: Mon, 20 Jan 92 10:06:56 CST
Message-Id: <9201201606.AA17227@cadsun.corp.mot.com>
Received: by munich.srd.mot (4.1/SMI-4.1) id AA00538;
          Mon, 20 Jan 92 10:06:54 CST
To: info-hol@edu.ucdavis.cs
Subject: Query about testing

What is the difference between formal verification and formal testing
of specifications?  From a mathematical perspective, it looks the
same.  However, there are probably some differences wrt completeness.

Given a specification of system, can a theorem prover be used at any
stage to perform specification-dependent testing?  Formal testing is
mostly like to fault-detection, where one wants to detect undesirable
states of a computation.

I'd welcome pointers to published papers or technical reports in this
area.

Thanks for any related flames or input.

--Ramu Iyer

Email: ramu@mot.com