Abtstract Interpretation Using Typed Decision Graphs

Laurent Mauborgne.
Abstract Interpretation Using Typed Decision Graphs.
Science of Computer Prgramming, 31(1):91--112, May 1998.
Compressed PostScript (106K), DVI (102K), PDF (290K).
Abstract: This article presents a way of implementing abstract interpretations that can be very efficient. The improvement lies in the use of a symbolic representation of boolean functions called Typed Decision Graphs (TDGs), a refinement of Binary Decision Diagrams. A general procedure for using this representation in abstract interpretation is given; we examine in particular 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 interpretations will not fail due to insufficient memory. This approach is illustrated on strictness analysis of higher-order functions, showing a great increase in efficiency.

\bibitem{mauborgne98}
{\sc Mauborgne, L.}
\newblock Abstract interpretation using typed decision graphs.
\newblock {\em Science of Computer Programming 31}, 1 (May 1998), 91--112.

@article{mauborgne98,
author = "Laurent Mauborgne",
title  = "Abstract interpretation using typed decision graphs",
journal = "Science of Computer Programming",
year   = 1998,
volume = 31,
number = 1,
pages  = "91--112",
month  = "May" }

Email: Laurent.Mauborgne@ens.fr