Re: Abstract Interpretation Query

>What I want to know is: has anybody applied it to everyday imperative
>languages in real life (i.e. to languages like Pascal, C, and
>analyses like type analysis, data flow analysis etc.)?


Of course ! And for a long time. For instance operational abstract
interpretation (AI) a la [Cousots77a] and in particular the interval
analysis for integer variables described in this paper and the alias
analysis described in [Cousots77b] have both successfuly been applied to
the automatic analysis of Ada programs (which certainly qualifies as a
real programming language), in order to safely eliminate array bound
checking and overflow checking. The analysis has been implemented by
people from ALSYS and integrated in a real production compiler for Ada.
This was described in a paper written by E. Morel and published by
Cambridge University Press (not sure) sometime between 82 and 86 in the
proceedings of a course on compilers that took place at INRIA, edited by
B. Lorho which I do not have at hand right now. For a survey on how to
apply these particular AI techniques and others to imperatives programming
languages, see [Cousots77c].


>If so, what were your experiences with Abstract Interpretation?


My Phd subject was alias analysis for languages with structured data,
imperative operations, polymorphism and higher-order functions. This
potentially covers a large spectrum of programming languages including ML
and Ada.


My experience has been very satisfactory so far, both theoretically and
practically as I end up with several algorithms, including one that
discovers a new kind of aliasing information not discovered by existing
algorithms.


What we should remember is what those who pioneered abstract
interpretation (Cousot & Cousot) had in mind, as formulated by F.
Nielson:


AI = DFA + proofs


or in other words:


ABSTRACT INTERPRETATION = DATA FLOW ANALYSIS + CORRECTNESS.


Correctness proofs set up a connection between the exact semantics
(operational a la Cousot or denotational a la Mycroft & Nielson) of the
programming language and the data flow analysis. Mathematically this
usually involves lattice theory, transfinite and fixpoint induction and
Galois connections.


I think it is important to have this in mind, and lots of people do not
seem to know that abstract interpretation is strongly connected to data
flow analysis, including researchers from both fields: abstract
abstraction and data flow analysis.


Sincerely,


Alain Deutsch.
----
Alain Deutsch -- School of Computer Science
Carnegie Mellon University, Pittsburgh, PA 15213-3891, USA.
Email: deutsch@cs.cmu.edu, Phone: (412) 268-6658, Fax: (412) 681-5739.


------------------------------------------------------------------------------
REFERENCES:


@InProceedings{Cousots77a,
    author = "Cousot,P. and Cousot, R.",
    title = "Abstract Interpretation~: a unified lattice model for
static analysis of programs by construction of
approximation of fixpoints",
    booktitle = "Fourth Annual ACM Symp. on Principles of Programming Languages",
    year = "1977",
    pages = "238--252",
    address = "Los Angeles",
    month = jan
}


@InProceedings{Cousots77b,
    author = "Cousot,P. and Cousot,R.",
    title = "Static determination of dynamic properties of
recursive procedures",
    booktitle = "Working Conf. on Formal Description of
Programming Concepts",
    year = "1977",
    organization= "IFIP WG 2.2",
    publisher = "North-Holland",
    address = "St-Andrews,Canada",
    month = aug
}


@Article{Cousot77c,
    author = "Cousot,P. and Cousot,R.",
    title = "Static determination of dynamic properties of generalized
     type unions",
    journal = "SIGPLAN Notices",
    year = 1977,
    volume = 12,
    number = 3,
    pages = "77--94",
    month = mar
}


@Article{Nielson89,
    author = "Nielson,F.",
    title = "Two-level semantics and abstract interpretation",
    journal = "Theoretical Computer Science",
    year = 1989,
    volume = 69,
    pages = "117-242",
    month = dec
}
--

Return to the comp.compilers page.
Search the comp.compilers archives again.