From: Jon Jacky Subject: Re: Yes, proof checkers exist! Date: 28 Dec 2000 10:28:09 -0800 Newsgroups: sci.math Summary: [missing] Steve Leibel 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/