P. Cousot , A Scalable Segmented Decision Tree Abstract Domain

Patrick Cousot
Patrick Cousot
A Scalable Segmented Decision Tree Abstract Domain
Amir Pnueli Memorial Symposium, CIMS, NYU, New York, NY, USA, May 7—9, 2010
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.
Joint work with Radhia Cousot and Laurent Mauborgne
Slides of the 60 mn presentation (to be used with Acrobat Reader):
- .pdf, 1 slide per page (4.8 Mb)
- .pdf, 4 slide per page (4.8 Mb)

Bibliographic reference:

\bibitem{Cousot-APM-2010-05-07--09}
P.~Cousot.
\newblock A Scalable Segmented Decision Tree Abstract Domain.
\newblock Amir Pnueli Memorial Symposium, CIMS, NYU, New York, NY, USA,	May 7--9, 2010.

@inProceedings{Cousot-APM-2010-05-07--09,
   author =    {P.~Cousot},
   title =     {A Scalable Segmented Decision Tree Abstract Domain,
   booktitle = {Amir Pnueli Memorial Symposium},
   address =   {CIMS, NYU, New York, NY, USA},
   month =     {May 7--9},
   year =      {2010},
}

Copyright notice
Last modified: Monday, 07-May-2012 17:51:02 EDT