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
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
A2 - Manna, Zohar
A2 - Peled, Doron A.
ER -