Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!rex!ukma!usenet.ins.cwru.edu!abvax!iccgcc!kambic
From: kambic@iccgcc.decnet.ab.com
Newsgroups: comp.software-eng
Subject: Re: Proofs (was: Global program state.)
Message-ID: <2829.279332ea@iccgcc.decnet.ab.com>
Date: 15 Jan 91 21:50:50 GMT
References: <2474@motcsd.csd.mot.com> <10370@lanl.gov> <1070@tetrauk.UUCP> <1991Jan11.175952.10978@pdn.paradyne.com> <14849@megatest.UUCP>
Lines: 20

In article <14849@megatest.UUCP>, pat@megatest.UUCP (Patrick Powers) writes:
> Harlan Mills has made studies that show that functional verification,
> as opposed to Hoare's axiomatic verification, is helpful in producing
> reliable software.  I've tried these techniques informally and found
> that quite helpful in producing a large system.  There was a cover 
> article about them in IEEE Software in about 1987 or 86.
> -- 
> --
In addition, there was a recent bit of work done at Ames Research Center (NASA) 
that examined the use of a cleanroom technique in developing software.  I am
currently beating my head against my file cabinet because I loaned the file to
someone else.  The basis of the study is the use of paper verification
techniques in sw development.  The claim is great success for the series of
projects studied (better, faster, cheaper).  It was done in conjunction with
the U of Maryland.  I believe that one of the lead authors, if not the lead, is
Dr. Victor Basili at UM.  You could probably call NASA or UM to get a copy of
the paper.  I cannot remember where it was published.  Talk about a need for
duplicate files!

GXKambic