Junjie Chen and Patrick Cousot, A Binary Decision Tree Abstract Domain Functor

Junjie Chen and Patrick Cousot.
A Binary Decision Tree Abstract Domain Functor
In Proceedings of the 22nd International Symposium on Static Analysis, Sandrine Blazy and Thomas Jensen (Eds), Saint Malo, France, September 12-14, 2015. LNCS 9291, pp. 36—53, © Springer, 2015.
Paper:
- PDF (17.2 MB)
Slides of the 25mn presentation at SAS'2015:
- 4 slides per landscape page, (12.9 Mb)
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.
Keywords:
Abstract domain, Abstract domain functor, Abstract interpretation, Binary decision tree, Galois connection, Extrapolation, Interpolation, Narrowing, Soundness, Static analysis, Widening.

Bibliographic reference:

@inproceedings{DBLP:conf/sas/ChenCousot15,
  author    = {Junjie Chen and
               Patrick Cousot},
  title     = {A Binary Decision Tree Abstract Domain Functor},
  booktitle = {Static Analysis - 22nd International Symposium, {SAS} 2015, Saint-Malo,
               France, September 9-11, 2015, Proceedings},
  pages     = {36--53},
  year      = {2015},
  crossref  = {DBLP:conf/sas/2015},
  url       = {http://dx.doi.org/10.1007/978-3-662-48288-9_3},
  doi       = {10.1007/978-3-662-48288-9_3},
}
@proceedings{DBLP:conf/sas/2015,
  editor    = {Sandrine Blazy and
               Thomas Jensen},
  title     = {Static Analysis - 22nd International Symposium, {SAS} 2015, Saint-Malo,
               France, September 9-11, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9291},
  publisher = {Springer},
  year      = {2015},
  url       = {http://dx.doi.org/10.1007/978-3-662-48288-9},
  doi       = {10.1007/978-3-662-48288-9},
  isbn      = {978-3-662-48287-2},
}

copyright notice, Springer copyright notice
Last modified: Thu Sep 17 13:58:18 EDT 2015