Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!pacific.mps.ohio-state.edu!zaphod.mps.ohio-state.edu!mips!apple!well!nagle
From: nagle@well.UUCP (John Nagle)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <15446@well.UUCP>
Date: 10 Jan 90 06:38:51 GMT
References: <7578@hubcap.clemson.edu> <25728@cup.portal.com> <4760@itivax.iti.org>
Reply-To: nagle@well.UUCP (John Nagle)
Lines: 40


      There are several verifiers available, none widely so.  I've been
out of this field for a few years, so this isn't current information.

      The Gypsy system, developed by Don Good and various others at the
University of Texas, is a code-level verifier and compiler for small
real-time programs.  The verification system ran on a Symbolics when
I last saw it.

      Robert Boyer and Jay Moore have a startup company in Austin called
Computational Logic, Inc., and they are working in this area.

      The Pascal-F Verifier, the system I worked on, can be distributed
to academic sites.  It's a code-level verifier for a real-time dialect
of Pascal.  The compiler, which targeted the Intel 8061, is not available.
The verifier is written in Berkeley Pascal and Franz LISP and runs on
VAXen and Suns.  It hasn't been used in years, but I could provide a copy
if someone is serious about bringing it up.  See the paper, "Practical
Program Verification", in POPL '83, for more information.  What it
basically undertakes to verify is that the program won't crash at
run time and that critical assertions and invariants are preserved.
Where real-time control is involved, these tend to be the crucial issues.
This system was never used for its intended purpose, verifying engine
control programs for automobiles, because the reliablity of those
programs turned out not to be a serious problem in practice.

      A serious verifier is about as complicated as a serious optimizing
compiler.  It's much more complicated than a simple compiler.  Many
workers in the field grossly underestimated the size of the implementation
required.

      Formal specifications turned out to be a dead end because they were
nearly as large as the program they specified and much harder to work on,
since you couldn't run them.  But where you can specify some desired
properties, such as real-time constraints, termination, numeric values
staying within the proper limits, and such, machine proof is quite 
feasible.


					John Nagle