ANNOUNCE: New white paper available on www.sparkada.com

ANNOUNCE: New white paper available on www.sparkada.com

[Rod Chapman]

A new white paper entitled "SPARK and Abstract Interpretation"
is now available for download on www.sparkada.com

The introduction reads:

"Recently, there has been significant interest in the use of Abstract
Interpretation (AI) technology in the static analysis of critical
software. A number of AI-based tools exist, but some of their marketing
suffers from a level of hyperbole that is at best optimistic, and
at worst somewhat irresponsible.

There have also been some attempts to compare AI-based static analysis
tools with the analysis implemented by the SPARK language and the SPARK
Examiner toolset. The aim of this white paper is to dispel some of the
common myths and to avoid potential confusion with customers."

I'm sure many readers of c.l.a might be interested in this.

Yours,
 Rod Chapman
 SPARK Team
 Praxis Critical Systems
 sparkinfo@praxis-cs.co.uk

Re: ANNOUNCE: New white paper available on www.sparkada.com

[Hambut]

Thanks, this is very interesting Rod.

Do you have any links to description of what Abstract Interpretation
is - i.e. what is it based on?

This would help me to better understand the points you make in the
white paper.

Cheers,

Hambut.

rod@praxis-cs.co.uk (Rod Chapman) wrote in message news:<ba18d5cb.0109210556.28833470@posting.google.com>...
> A new white paper entitled "SPARK and Abstract Interpretation"
> is now available for download on www.sparkada.com
> 
> The introduction reads:
> 
> "Recently, there has been significant interest in the use of Abstract
> Interpretation (AI) technology in the static analysis of critical
> software. A number of AI-based tools exist, but some of their marketing
> suffers from a level of hyperbole that is at best optimistic, and
> at worst somewhat irresponsible.
> 
> There have also been some attempts to compare AI-based static analysis
> tools with the analysis implemented by the SPARK language and the SPARK
> Examiner toolset. The aim of this white paper is to dispel some of the
> common myths and to avoid potential confusion with customers."
> 
> I'm sure many readers of c.l.a might be interested in this.
> 
> Yours,
>  Rod Chapman
>  SPARK Team
>  Praxis Critical Systems
>  sparkinfo@praxis-cs.co.uk

Re: ANNOUNCE: New white paper available on www.sparkada.com

[Martin Dowie]

To avoid Rod the embarrassment of helping the opposition, I'll
assume he is talking about the likes of Polyspace, who can be
found at:

www.polyspace.com


Hambut <hfrumblefoot@yahoo.com> wrote in message
news:fb75c450.0109240045.472dc22f@posting.google.com...
> Thanks, this is very interesting Rod.
>
> Do you have any links to description of what Abstract Interpretation
> is - i.e. what is it based on?
>
> This would help me to better understand the points you make in the
> white paper.
>
> Cheers,
>
> Hambut.
>
> rod@praxis-cs.co.uk (Rod Chapman) wrote in message
news:<ba18d5cb.0109210556.28833470@posting.google.com>...
> > A new white paper entitled "SPARK and Abstract Interpretation"
> > is now available for download on www.sparkada.com
> >
> > The introduction reads:
> >
> > "Recently, there has been significant interest in the use of Abstract
> > Interpretation (AI) technology in the static analysis of critical
> > software. A number of AI-based tools exist, but some of their marketing
> > suffers from a level of hyperbole that is at best optimistic, and
> > at worst somewhat irresponsible.
> >
> > There have also been some attempts to compare AI-based static analysis
> > tools with the analysis implemented by the SPARK language and the SPARK
> > Examiner toolset. The aim of this white paper is to dispel some of the
> > common myths and to avoid potential confusion with customers."
> >
> > I'm sure many readers of c.l.a might be interested in this.
> >
> > Yours,
> >  Rod Chapman
> >  SPARK Team
> >  Praxis Critical Systems
> >  sparkinfo@praxis-cs.co.uk

Re: ANNOUNCE: New white paper available on www.sparkada.com

[Manuel Carro]

> Do you have any links to description of what Abstract Interpretation
> is - i.e. what is it based on?

    Basically it is a general means to analyze programs by mapping
them into an abstract value space.  As a simple example, all numbers
can be mapped to either 0, positive, or negative, and the builtin
operations be redefined accordingly, i.e., 

x * y = y * x,
(0) * _ = (0)
(+) * (+) = (+)
(+) * (-) = (-)
(-) * (-) = (-)
....

    The program is then run in the abstract domain, possibly several
times, until the information concerning the program does not change.
Then one might be able to infer that a variable is, e.g., always
positive at some point.  The good point is that having a finite
abtract domain (with some mathematical properties) ensures termination
of the analysis.  The bad point is that, of course, information is
lost both with respect to the actual program (I know that something is
positive, but that does not help me to get rid of a "X > 3" test), and
with respect to the abstract domain itself (i.e., I might end up with
a variable which has "any value").

    The abstract domain should be carefully chosen to reflect the
properties one wants to study.  The nice thing is that the analysis
algorithm can be made (in principle) generic and be used with any
abstract domain.

    There has been a lot of work in abstract interpretation in logic
and declarative languages.


-- 
          ||            Manuel Carro -- DLSIIS            ||
          ||           e-mail: mcarro@fi.upm.es           ||
          ||      http://lml.ls.fi.upm.es/~boris          ||
          ||    http://clip.dia.fi.upm.es/Software/Ciao   ||
          || Phone: +34 91 336-7455  FAX: +34 91 336-7412 ||

Re: ANNOUNCE: New white paper available on www.sparkada.com

[Ken Garlington]

"Manuel Carro" <boris@lml.ls.fi.upm.es> wrote in message
news:7sn13ksoux.fsf@salmon.ls.fi.upm.es...
:
: > Do you have any links to description of what Abstract Interpretation
: > is - i.e. what is it based on?
:
:     Basically it is a general means to analyze programs by mapping
: them into an abstract value space.

There is also a brief description at

http://www.polyspace.com/abstract.htm