Path: utzoo!attcan!uunet!samsung!think!snorkelwacker!apple!voder!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <19988@joshua.athertn.Atherton.COM>
Date: 19 Mar 90 17:23:35 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <18190@duke.cs.duke.edu> <1424@oravax.UUCP>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 22

Someone has suggested that we post programs, and let the verification 
folks try to verify them.  Sounds good to me.

I would like to see any of the following four programs verified:
GnuTar, GCC, GAWK, or G++.

All of them are real, and do useful things.  All are available in source
code.  And all have pretty well defined behaviors.  GCC uses the ANSI
standard, G++ and GAWK are based on books and some follow on technical 
reports, and I believe that GnuTar is based on the POSIX tar standard.  
GCC and G++ are both huge, but GAWK and GnuTar should be reasonably sized.

Is anyone willing to send them through a verification system?  
Ian, do you have the time for this?  If so please tell us such things
as the bugs you find, the time it took, the verification system and
methodology you used, the version of the program you verified, etc.
Also, send the results to the GNU people, I'm sure they'll be interested
in them.  If you can not verify one of these progams, please tell us
why.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822