Assertion Checking Unified

Abstract

We revisit the connection between equality assertion checking in programs and unification that was recently described in [GT06]. Using a general formalization of this connection, we establish interesting connections between the complexity of assertion checking in programs and unification theory of the underlying program expressions. In particular, we show that assertion checking is: These results generalize several recently published results and also establish several new results. In essence, they provide new techniques for backward analysis of programs based on novel integration of theorem proving technology in program analysis.