From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.6 required=5.0 tests=BAYES_05,INVALID_DATE
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,d2b8a512e0ded41b,start
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 1993-03-23 10:40:39 PST
Newsgroups: comp.lang.ada
Path: sparky!uunet!mcsun!sunic!psinntp!psinntp!scylla!davidg
From: davidg@oracorp.com (David Guaspari)
Subject: Re:  Ada Static Analysis Tools
Message-ID: <1993Mar23.155140.819@oracorp.com>
Sender: davidg@oracorp.com (David Guaspari)
Organization: ORA Corporation, Ithaca, New York
Date: Tue, 23 Mar 1993 15:51:40 GMT
Date: 1993-03-23T15:51:40+00:00
List-Id: <comp.lang.ada>

A no doubt incomplete list of people working on static analysis of Ada.

People working on formal verification of Ada code (aside from the
MALPAS bunch) include:

   ORA (my shop, brief advert below)
   Computational Logic, Inc. (try mksmith@cli.com)
   Aerospace Corporation, (try blevy@aerospace.aero.org)
   Program Validation, Ltd. (in the UK, can't find an e-mail address)

People working on more "mainstream" static analysis (data-flow
analysis, etc.) include:

   The Arcadia Project (lots of different universities involved,
      try clarke@cs.umass.edu)
   ORA (also advertised below)

----------


ORA stuff:

  Penelope is a system for formal specification and verification of
Ada code.  It aims at covering a very large subset of Ada (both
sequential and concurrent).  The most easily accessible description is
in 

     Formal verification of Ada programs
     David Guaspari, Carla Marceau, and Wolfgang Polak
     IEEE Transactions on Software Engineering, vol. 16, no. 9.
        September, 1990, pp. 1058-1075

The system described there is old, and much less capable than the
current system (in particular, the current system is able to do
nontrivial things with floating point computations and with generics).

For more information contact me: davidg@oracorp.com.

   We also have versions of various "lightweight tools" that warn
about possible occurrences of improper aliasing and incorrect order
dependences (with various other things, such as warning about
possibilities for erroneous execution, in the works).

For more information contact Cheryl Barbasch: cbarb@oracorp.com.

- David Guaspari
  davidg@oracorp.com