An analysis method for specialization of imperative programs is described in this paper. This analysis is an inter-procedural data flow method operating on control flow graphs and collecting information about program expressions. It applies to various procedural languages. The set of analyzed formulas includes equivalences between program expressions and constants, linear-ordering inequalities between program expressions and constants, equalities originating from some program assignments, and atomic constituents of controlling expressions of program branches. Analysis is executed by a worklist-based fixpoint algorithm which interprets conditional branches and ignores some impossible paths. This analysis algorithm incorporates a simple inference procedure that utilizes both positive and negative information. The analysis algorithm is shown to be conservative; its asymptotic time complexity is cubic. A polyvariant specialization of imperative programs, that is based on the information c...