Программный модуль построения, оптимизации и детерминированного воспроизведения доказательств с помощью суперпозиционных решателей и решателей формул в теориях
ВЕРИФИКАЦИЯ
Реализованный в программе набор методов и команд предназначен для использования при интерактивном доказательстве теорем в системе Isabelle/HOL. Они позволяют автоматически получать быстро воспроизводимые доказательства утверждений для более сложных случаев, в которых не сработал стандартный инструмент Sledgehammer, либо сгенерированное им доказательство воспроизводится неприемлемо длительное время. Также программа позволяет извлекать и анализировать частичные контрпримеры для выявления ошибок в формулировках утверждений. Являясь пакетом расширения для системы Isabelle/HOL, программа реализует набор методов доказательства (tsmt, topt, tmetis), команд (tlkp, tlki) и атрибутов (when, tsmt add/del, tsmt skolem, tsmt def, tsmt size) для оптимизации и детерминированного воспроизведения ядром Isabelle/Pure доказательств теорем, получаемых от решателей формул в теориях (Z3, CVC4, VeriT) и суперпозиционных решаталей (E-Propver, Vampire, Metis).
Автоматизация доказательства корректности программных систем и формальных моделей.
Петренко А. К.
заведующий отделом
Доктор физико-математических наук
Аветисян А. И.
ВРИО директора
50.05.17
Теоретические основы системного программного обеспечения
01.02.ET
COMPUTER SCIENCE, INFORMATION SYSTEMS
01.02.EX
COMPUTER SCIENCE, THEORY & METHODS
01.02.EW
COMPUTER SCIENCE, SOFTWARE ENGINEERING
Михаил
Мандрыкин
Усамович
Проектирование, разработка и реализация алгоритмов. Написание и отладка программы.
Алексей
Хорошилов
Владимирович
Проектирование алгоритмов.
МИНОБРНАУКИ РОССИИ
МИНИСТЕРСТВО НАУКИ И ВЫСШЕГО ОБРАЗОВАНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ
1187746579690
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные казенные учреждения
ИСП РАН
Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В.П. Иванникова Российской академии наук
1037700067327
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения