A binary decision tree abstract domain functor

Junjie Chen, Patrick Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 partitioning 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, transfer 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.

Original languageEnglish (US)
Title of host publicationStatic Analysis- 22nd International Symposium, SAS 2015, Proceedings
EditorsSandrine Blazy, Thomas Jensen
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783662482872
StatePublished - 2015
Event22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France
Duration: Sep 9 2015Sep 11 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other22nd International Static Analysis Symposium, SAS 2015

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A binary decision tree abstract domain functor'. Together they form a unique fingerprint.

Cite this