Assertion Verification Using Structural Invariants

The authors present a new assertion verification algorithm based on Structural Invariants (SI) computed by making a linear pass over the dominator tree of a program in SSA form. The 1-level SI at a program location is the conjunction of all dominating program statements viewed as constraints. For any k, they define a k-level SI by recursively strengthening the dominating joins of the 1-level SI with the (k -1)-level SI of the join's predecessors, thereby distinguishing k levels of nested conditionals. SI provide a sound, generic (No program-specific abstract domain required), scalable, and precise (Low false positive rate) algorithm for path sensitive assertion verification.