A binary decision tree abstract domain functor

Junjie Chen, Patrick Cousot

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

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 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
PublisherSpringer Verlag
Pages36-53
Number of pages18
Volume9291
ISBN (Print)9783662482872
DOIs
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)
Volume9291
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other22nd International Static Analysis Symposium, SAS 2015
CountryFrance
CitySaint-Malo
Period9/9/159/11/15

Fingerprint

Decision trees
Decision tree
Functor
Binary
Leaves
Path
Static analysis
Static Analysis
Vertex of a graph
Extrapolation
Transfer Function
Join
Transfer functions
Mathematical operators
Partitioning
Branch
Inclusion
Semantics
Trace
Dependent

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Chen, J., & Cousot, P. (2015). A binary decision tree abstract domain functor. In Static Analysis- 22nd International Symposium, SAS 2015, Proceedings (Vol. 9291, pp. 36-53). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291). Springer Verlag. https://doi.org/10.1007/978-3-662-48288-9_3

A binary decision tree abstract domain functor. / Chen, Junjie; Cousot, Patrick.

Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291 Springer Verlag, 2015. p. 36-53 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291).

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

Chen, J & Cousot, P 2015, A binary decision tree abstract domain functor. in Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. vol. 9291, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9291, Springer Verlag, pp. 36-53, 22nd International Static Analysis Symposium, SAS 2015, Saint-Malo, France, 9/9/15. https://doi.org/10.1007/978-3-662-48288-9_3
Chen J, Cousot P. A binary decision tree abstract domain functor. In Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291. Springer Verlag. 2015. p. 36-53. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-48288-9_3
Chen, Junjie ; Cousot, Patrick. / A binary decision tree abstract domain functor. Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291 Springer Verlag, 2015. pp. 36-53 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{65e3069002db489786cac2150eb3fd5c,
title = "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 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.",
author = "Junjie Chen and Patrick Cousot",
year = "2015",
doi = "10.1007/978-3-662-48288-9_3",
language = "English (US)",
isbn = "9783662482872",
volume = "9291",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "36--53",
booktitle = "Static Analysis- 22nd International Symposium, SAS 2015, Proceedings",

}

TY - GEN

T1 - A binary decision tree abstract domain functor

AU - Chen, Junjie

AU - Cousot, Patrick

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84946014966&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84946014966&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-48288-9_3

DO - 10.1007/978-3-662-48288-9_3

M3 - Conference contribution

SN - 9783662482872

VL - 9291

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 36

EP - 53

BT - Static Analysis- 22nd International Symposium, SAS 2015, Proceedings

PB - Springer Verlag

ER -