Найдич Д. Э. Модели, вычисления и методы доказательства индуктивных утверждений для эквациональных спецификаций с частичными функциями

Объект исследования: Эквациональные спецификации с частичными функциями. Цель исследования: Разработка новых высоко автоматизированных исчислений для доказательства индуктивных утверждений. Методы исследования и аппаратура: Теория эквациональных спецификаций, принципы "безиндукционной" индукции и индуктивного пополнения. Теоретические результаты и новизна: Предложены новые высоко автоматизированные исчисления для доказательства индуктивных положений. Практические результаты и новизна: С помощью разработанных исчислений решена задача верификации компилятора. Предмет и степень внедрения: Автоматизированные методы верификации спецификации (техническое задание на НИР согласно решению ДКНТ Украины). Эффективность внедрения: Качественное повышение надежности проектирования программных систем. Сфера (область) использования: Проектирование сложных программных систем.