We present Structural Invariants (SI), a new technique for incrementally overapproximating the verification condition (VC) by making a linear pass over the dominator tree of the program in single static assignment form. The 1-level SI at a program location is the conjunction of all dominating program statements viewed as constraints. For any $k$, we define a k-level SI by recursively strengthening the dominating join points of the 1-level SI with the (k-1)-level SI of the join's predecessors, thereby providing a tunable selector to add path-sensitivity incrementally. By ignoring program paths, the size of the SI and correspondingly the time to discharge the validity query remains small, allowing the technique to scale to large programs. We show experimentally that for a set of open-source programs totaling 570K lines, and properties for which specialized analyses have been previously devised, our method provides an automatic and scalable algorithm with a low false positive rate.
Proceedings of the 13th International Static Analysis Symposium (SAS), 2006.