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.
\bibitem{ccm10}
Patrick Cousot, Radhia Cousot, and Laurent Mauborgne.
\newblock A scalable segmented decision tree abstract domain.
\newblock In Z.~Manna and D.~Peled, editors, {\em Pnueli Festschrift}, volume
6200 of {\em Lecture Notes in Computer Science}, pages 72--95, Heidelberg,
2010. Springer-Verlag.
@inproceedings{ccm10,
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
title = "A Scalable Segmented Decision Tree Abstract Domain",
booktitle = "Pnueli Festschrift",
editor = "Z. Manna and D. Peled",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = "6200",
year = 2010,
pages = "72--95",
address = "Heidelberg"
}