Deciding linear inequalities by computing loop residues

ABSTRACT V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUes ofthe form x _< y + c can be decided quickly by examining the loops m certain graphs Pratt's method is generahzed, first to real feaslbdlty of mequahues m two variables and arbitrary coefficients, and ultimately to real feaslbdlty of arbitrary sets of hnear mequahtles The method is well suited to apphcatlons m program verification KEY WORDS AND PHRASES theorem proving, decision procedures, program venficauon, linear programmmg CRCATEGORIES 3 15,369,521,532,541 1. lntroductton Procedures for deciding whether a given set of l inear inequalities has solutions often play an important role in deductive systems for program verification. Array bounds checks and tests on index variables are but two of the many common programming constructs that give rise to formulas involving inequalities. A number of approaches have been used to decide the feasibdity of sets of inequalities [3, 8, 9, 16, 22], ranging from goal-driven rewriting mechanisms [27] to the powerful simplex techniques [8