Assertion Checking Unified

MSR-TR-2006-99 |

This paper establishes an interesting connection between assertion checking in programs and unification in the theory underlying the program expressions. Using this connection, we describe how unification algorithms from theorem proving can be used to perform backward analysis over programs for assertion checking. Interestingly enough, this connection also helps prove hardness results for assertion checking for classes of program abstractions. In particular, we show (a) Assertion checking is PTIME for programs with nondeterministic conditionals that use expressions from a strict unitary theory. (b) Assertion checking is coNP-hard for programs with nondeterministic conditionals that use expressions from a bitary theory. (c) Assertion checking is decidable for programs with disequality guards that use expressions from a convex finitary theory. (d) Summary computation for interprocedural analysis can be performed using backward analysis, enabled with unification, on generic assertions. This helps generalize result (a) to interprocedural analysis. These results generalize several recently published results using a uniform framework. They also provide several new results, and partially solve the long standing open problem of interprocedural global value numbering. In essence, they provide new techniques for backward analysis of programs based on novel integration of theorem proving technology in program analysis.