A scalable segmented decision tree abstract domain

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

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

Abstract

The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity. Building upon packed binary decision trees to handle disjunction in tests, loops and procedure/function calls and array segmentation to handle disjunctions in array content analysis, we introduce segmented decision trees to allow for more expressivity while mastering costs via widenings.

Original languageEnglish (US)
Title of host publicationTime for Verification - Essays in Memory of Amir Pnueli
Pages72-95
Number of pages24
Volume6200 LNCS
DOIs
StatePublished - 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6200 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Fingerprint

Static Analysis
Decision trees
Decision tree
Program Verification
Content Analysis
Formal methods
Program Analysis
Interleaving
Formal Methods
Static analysis
Costs
Explosion
Thread
Enumeration
Explosions
Immediately
Scalability
Concurrent
Segmentation
Binary

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., Cousot, R., & Mauborgne, L. (2010). A scalable segmented decision tree abstract domain. In Time for Verification - Essays in Memory of Amir Pnueli (Vol. 6200 LNCS, pp. 72-95). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6200 LNCS). https://doi.org/10.1007/978-3-642-13754-9_5

A scalable segmented decision tree abstract domain. / Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent.

Time for Verification - Essays in Memory of Amir Pnueli. Vol. 6200 LNCS 2010. p. 72-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6200 LNCS).

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

Cousot, P, Cousot, R & Mauborgne, L 2010, A scalable segmented decision tree abstract domain. in Time for Verification - Essays in Memory of Amir Pnueli. vol. 6200 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6200 LNCS, pp. 72-95. https://doi.org/10.1007/978-3-642-13754-9_5
Cousot P, Cousot R, Mauborgne L. A scalable segmented decision tree abstract domain. In Time for Verification - Essays in Memory of Amir Pnueli. Vol. 6200 LNCS. 2010. p. 72-95. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-13754-9_5
Cousot, Patrick ; Cousot, Radhia ; Mauborgne, Laurent. / A scalable segmented decision tree abstract domain. Time for Verification - Essays in Memory of Amir Pnueli. Vol. 6200 LNCS 2010. pp. 72-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{b2552cf96be2425faeaa105e25f92777,
title = "A scalable segmented decision tree abstract domain",
abstract = "The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity. Building upon packed binary decision trees to handle disjunction in tests, loops and procedure/function calls and array segmentation to handle disjunctions in array content analysis, we introduce segmented decision trees to allow for more expressivity while mastering costs via widenings.",
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
year = "2010",
doi = "10.1007/978-3-642-13754-9_5",
language = "English (US)",
isbn = "3642137539",
volume = "6200 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "72--95",
booktitle = "Time for Verification - Essays in Memory of Amir Pnueli",

}

TY - GEN

T1 - A scalable segmented decision tree abstract domain

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Mauborgne, Laurent

PY - 2010

Y1 - 2010

N2 - The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity. Building upon packed binary decision trees to handle disjunction in tests, loops and procedure/function calls and array segmentation to handle disjunctions in array content analysis, we introduce segmented decision trees to allow for more expressivity while mastering costs via widenings.

AB - The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity. Building upon packed binary decision trees to handle disjunction in tests, loops and procedure/function calls and array segmentation to handle disjunctions in array content analysis, we introduce segmented decision trees to allow for more expressivity while mastering costs via widenings.

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

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

U2 - 10.1007/978-3-642-13754-9_5

DO - 10.1007/978-3-642-13754-9_5

M3 - Conference contribution

AN - SCOPUS:77955037046

SN - 3642137539

SN - 9783642137532

VL - 6200 LNCS

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

SP - 72

EP - 95

BT - Time for Verification - Essays in Memory of Amir Pnueli

ER -