Static analysis in disjunctive numerical domains

Sriram Sankaranarayanan, Franjo Ivančić, Ilya Shlyakhter, Aarti Gupta

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

51 Scopus citations

Abstract

The convexity of numerical domains such as polyhedra, octagons, intervals and linear equalities enables tractable analysis of software for buffer overflows, null pointer dereferences and floating point errors. However, convexity also causes the analysis to fail in many common cases. Powerset extensions can remedy this shortcoming by considering disjunctions of predicates. Unfortunately, analysis using powerset domains can be exponentially more expensive as compared to analysis on the base domain. In this paper, we prove structural properties of fixed points computed in commonly used powerset extensions. We show that a fixed point computed on a powerset extension is also a fixed point in the base domain computed on an "elaboration" of the program's CFG structure. Using this insight, we build analysis algorithms that approach path sensitive static analysis algorithms by performing the fixed point computation on the base domain while discovering an "elaboration" on the fly. Using restrictions on the nature of the elaborations, we design algorithms that scale polynomially in terms of the number of disjuncts. We have implemented a light-weight static analyzer for C programs with encouraging initial results.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 13th International Symposium, SAS 2006, Proceedings
PublisherSpringer Verlag
Pages3-17
Number of pages15
ISBN (Print)3540377565, 9783540377566
DOIs
StatePublished - 2006
Event13th International Symposium on Static Analysis, SAS 2006 - Seoul, Korea, Republic of
Duration: Aug 29 2006Aug 31 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4134 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Symposium on Static Analysis, SAS 2006
CountryKorea, Republic of
CitySeoul
Period8/29/068/31/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Static analysis in disjunctive numerical domains'. Together they form a unique fingerprint.

Cite this