Анотація. Представлено новий метод доведення інваріантності системи лінійних нерівностей для ітераційних циклів, визначених над полем раціональних чисел з лінійним оператором у тілі циклу. Метод враховує передумову циклу у вигляді системи лінійних нерівностей. Розгляд обмежено випадком, коли усі власні значення лінійного оператора є дійсними. Метод базується на обчисленні числа ітерацій циклу, після виконання яких інваріантність системи лінійних нерівностей або забезпечується, або спростовується. Метод використовує представлення лінійного оператора у його жордановій формі.

Ключові слова: статичний аналіз програм, лінійні інваріанти циклів, інваріантні системи лінійних нерівностей.