P. Cousot & R. Cousot, Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation

Patrick Cousot & Radhia Cousot.
Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation.
In Conference Record of FPCA '95 SIGPLAN/SIGARCH/WG2.8 Conference on Functional Programming and Computer Architecture, pages 170--181, La Jolla, California, U.S.A., 25-28 June 1995. ACM Press, New YYork, U.S.A.
Compressed PostScript (237 K)
Also available by ftp on lix.polytechnique.fr in pub/ESPRIT/LOMAPS as LOMAPS-ENS-X-9.ps.gz.
ACM Digital Library
Abstract: Grammar-based program analysis à la Jones and Muchnick and set-constraint-based program analysis à la Aiken and Heintze are static analysis techniques that have traditionally been seen as quite different from abstract-interpretation-based analyses, in particular because of their apparent non-iterative nature. For example, on page 18 of N. Heintze thesis, it is alleged that ``The finitary nature of abstract interpretation implies that there is a fundamental limitation on the accuracy of this approach to program analysis. There are decidable kinds of analysis that cannot be computed using abstract interpretation (even with widening and narrowing). The set-based analysis considered in this thesis is one example''.
On the contrary, we show that grammar and set-constraint-based program analyses are similar abstract interpretations with iterative fixpoint computation using either a widening or a finitary grammar/set-constraints transformer or even a finite domain for each particular program.
The understanding of grammar-based and set-constraint-based program analysis as a particular instance of abstract interpretation of a semantics has several advantages. First, the approximation process is formalized and not only explained using examples. Second, a domain of abstract properties is exhibited which is of general scope. Third, these analyses can be easily combined with other abstract-interpretation-based analyses, in particular for the analysis of numerical values. Fourth, they can be generalized to very powerful attribute-dependent and context-dependent analyses. Finally, a few misunderstandings may be removed.
Slides of the 25mn FPCA'95 talk are available for retroprojection, ghostview, printing.

\bibitem{CousotCousot95-1}
P.~Cousot and R.~Cousot.
\newblock Formal Language, Grammar and Set-Constraint-Based 
   Program Analysis by Abstract Interpretation.
\newblock In \emph{SIGPLAN/SIGARCH/WG2.8 7$^{\mathrm{th}}$
   Conference on Functional Programming and Computer Architecture,
   FPCA'95}. La Jolla, California,  U.S.A{.}, pages 170--181. 
   ACM Press, New York, U.S.A{.}, 25-28 June 1995. 

@inproceedings{CousotCousot95-1,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Formal Language, Grammar and Set-Constraint-Based Program 
                Analysis by Abstract Interpretation},
   pages =     {170--181},
   booktitle = {Proceedings of the Seventh ACM Conference on Functional 
                Programming Languages and Computer Architecture},
   address =   {La Jolla, California},
   publisher = {ACM Press, New York, NY},
   month =     {25--28 June},
   year =      1995,
}

copyright notice
Last modified: Monday, 04-Jan-2010 12:31:53 CET