From: Jon Jacky <jon@bilbo.radonc.washington.edu>
Subject: Re: Yes, proof checkers exist!
Date: 28 Dec 2000 10:28:09 -0800
Newsgroups: sci.math
Summary: [missing]

Steve Leibel <stevel@bluetuna.com> writes:

> In article <92dpgk$1i6$1@newsflash.concordia.ca>, mckay@cs.concordia.ca 
> (MCKAY john) wrote:
> 
> > [SNIP]
> > Why do we not have decent usable proof checkers today?  One can in
> > principle check segments of programs in certain languages - Why is
> > there nothing commercial out there? Or is there?
> > 
> 
> Well there you have it.  The difference between "in principle" and 
> "commercial."  Long way from one to the other.

Here are two well-engineered systems that have been used to do
significant proofs in industry.  Both are available for free, so
perhaps they are not themselves "commercial" --- but commercial folks
use them.

 PVS at http://pvs.csl.sri.com/
 Z/EVES at http://www.ora.on.ca/z-eves/welcome.html

For many other systems see

 http://archive.comlab.ox.ac.uk/formal-methods.html

-- 

Jonathan Jacky				jon@radonc.washington.edu
Radiation Oncology, Box 356043		voice:	(206)-598-4117
University of Washington		FAX:	(206)-598-6218	
Seattle, Washington  98195-6043	USA

http://www.radonc.washington.edu/prostaff/jon/