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
EditorsZohar Manna, Doron A. Peled
Pages72-95
Number of pages24
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)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'A scalable segmented decision tree abstract domain'. Together they form a unique fingerprint.

Cite this