Abstract Interpretation Using Typed Decision Graphs

Interpretation Using Typed Decision Graphs Laurent Mauborgne LIENS, ´Ecole Normale Sup´erieure, 45 rue d’Ulm, 75230 Paris cedex 05, France 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 gencedure 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 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.

• Type: Journal
• Year: 1998
• Where: SCP
• Authors: Laurent Mauborgne
• Keywords: Abstract Interpretation, Decision Graphs, Graphs Laurent Mauborgne, SCP 1998