Deciding Linear Inequalities by Computing Loop Residues.
Robert E. Shostak · 1978
V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUes of the 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 lntroducttonProcedures for deciding whether a given set of linear 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] of linear programming.Some simple methods are well suited to the small, trivial problems that most often arise, but are insufficiently general.Full-scale simplex techniques, on the other hand, are general and fast for medium to large problems, but do not take advantage of the trivial structure of the small problems (revolving only a few variables and equations) encountered most frequently in program verification and related applications.The algorithm presented here retains the generality needed in the exceptional case, without sacrifice of speed and simplicity in the more typical small problem case.It builds on V. R. Pratt's observation [18, 20] that most of the inequalities that arise from verification conditions are of the form x _< y + c, where x and y are variables and c is a constant.Pratt showed that a conjunction of such inequalities can be decided quickly by examining the loops of a graph constructed from the inequalities of the conjunction.We generalize this approach, first to inequalities with no more