Описаны методы доказательства правильности программ в системе инсерционного моделирования, ее архитектура и функциональные возможности, даны сведения о нем. Рассморена инсерционная машина метода Флойда, методы проверки выполнимости формул и их использование при доказательстве правильности программ.

Управляющие системы и машины [Текст] : междунар. научный журнал / НАН Украины. Междунар.науч.-учеб.центр информ.технологий и систем. Ин-т киберн.им.В.М.Глушкова. — статьи публ.на русск.укр. и англ .яз. — К.

• УДК // Обчислювальна математика. Числовий аналіз