Disjunctive invariants for modular static analysis

Abstract

We study the application of modular static analysis to prove program safety and detection of program errors. The analyses proposed in this thesis benefit from the relationship between a modular analyzer and a precise disjunctive domain. A modular analyzer requires a precise abstract domain to reason about the symbolic method inputs. On the other hand, a modular analyzer has a local scope and therefore favors more complex invariants than those that are usually involved in global analyzers. To handle the challenges of disjunctive analyses, we introduce the notion of affinity to characterize how closely related is a pair of disjuncts. We have implemented a static analyzer based on the disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost.