Abtstract Interpretation Using TDGs

Laurent Mauborgne.
Abstract Interpretation Using TDGs.
In B. Le Charlier, editor, Static Analysis Symposium (SAS'94), volume 864 of Lecture Notes in Computer Science, pages 363--379.
Springer-Verlag, 1994.
Compressed PostScript (64K)
Abstract: This paper intends to give an efficient way of implementing abstract interpretations. The idea is to use a good symbolic representation of boolean functions, TDGs, a refinement of Binary Decision Diagrams. A general way of using this representation in abstract interpretation is given, in particular we examine the possibility of encoding higher order functions into TDGs. Moreover, this representation is used to design a widening operator based on the size of the objects represented, so that abstract interpretation will not fail due to insufficient memory. This approach is illustrated on strictness analysis of higher-order functions, showing a great increase of efficiency.

\bibitem{mauborgne94}
{\sc Mauborgne, L.}
\newblock Abstract interpretation using {TDGs}.
\newblock In {\em Static Analysis Symposium (SAS'94)\/} (1994), B.~L. Charlier,
  Ed., vol.~864 of {\em Lecture Notes in Computer Science}, Springer-Verlag,
  pp.~363--379.

@inproceedings{mauborgne94,
author = "Laurent Mauborgne",
title  = "Abstract Interpretation Using {TDGs}",
booktitle = "Static Analysis Symposium (SAS'94)",
year   = 1994,
volume = 864,
editor = "B. Le Charlier",
pages = "363--379",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag" }

Email: Laurent.Mauborgne@ens.fr