A Binary Decision Tree Abstract Domain Functor

Abstract. We present an abstract domain functor whose elements are binary decision trees. It is parameterized by decision nodes which are a set of boolean tests appearing in the programs and by a numerical or symbolic abstract domain whose elements are the leaves. We first define the branch condition path abstraction which forms the decision nodes of the binary decision trees. It also provides a new prospective on parti-tioning the trace semantics of programs as well as separating properties in the leaves. We then discuss our binary decision tree abstract domain functor by giving algorithms for inclusion test, meet and join, trans-fer functions and extrapolation operators. We think the binary decision tree abstract domain functor may provide a flexible way of adjusting the cost/precision ratio in path-dependent static analysis.