Abstract interpretation using typed decision graphs

AbstractThis 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