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

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