🚀 go-pugleaf

nagle@well.UUCP (John Nagle) writes:
> ... I've been
>out of this field for a few years, so this isn't current information.
    Me too, but I'll provide what corrigenda & additional bits I can
anyway.

>      The Gypsy system, developed by Don Good and various others at the
>University of Texas, ...
>      Robert Boyer and Jay Moore have a startup company in Austin called
>Computational Logic, Inc., and they are working in this area.
   Last time I was in Austin (well, only), Don Good was the person we were
visting at CLInc.  I'm not sure if all three are still there, but CLInc
should be a good source for current info, and maybe even tools.

Susan Gerhart's group at MCC (also Austin) isn't scheduled to have anything
usable for a few years yet, I hear, but is also a group to watch.

Anyone in Austin listening and care to comment?

A group working on a verifiable Euclid Derivative & support tools 
which they were calling Verdi, was spun-off from IPSharpe Ottowa; 
the most flamboyant personality on the team was Dan Cragen, who sat
in on the Kemmerer study of verification techonology a few years back.
I don't know what name they are doing business as, but
when they come to market, if they manage to pickup some specification
libraries (such as MIT's LARCH project's archives), it will be usable.
(I took their training course)

-- bill ricker, formerly a professional paranoid in computer security
                for the taxpayers