Abstract. A new method is presented to prove the invariance of simultaneous linear inequalities for iteration loops defined over the field of rational numbers with linear operator in the loop body. The method takes into account the loop precondition in the form of simultaneous linear inequalities. The considerations are limited by the case of real eigenvalues of the linear operator. The method is based on computing the number of cycle iterations whose execution either ensures or disproves the invariance of the system of linear inequalities. The method uses the representation of linear operator in its Jordan form.

Keywords: static program analysis, linear invariant of a loop, invariant system of linear inequalities.