Static Analysis in Disjunctive Numerical Domains
Sriram Sankaranarayanan (NEC Laboratories America), Franjo Ivancic (NEC Laboratories America), Ilya Shlyakhter (NEC Laboratories America)and Aarti Gupta (NEC Laboratories America)
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.