Re: Ada Static Analysis Tools

[davidg@oracorp.com (David Guaspari)]

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