|
ИСТИНА |
Войти в систему Регистрация |
Интеллектуальная Система Тематического Исследования НАукометрических данных |
||
Дедуктивная верификация свойств монадических функций смарт-контрактов на трассахкурсовая работа (Специалист)
- Научный руководитель: Миронов А.М.
- Автор: Зиборов Кирилл Викторович
- Тип: Специалист
- Организация, в которой проходила защита: МГУ имени М.В. Ломоносова
- Кафедра: Кафедра математической теории интеллектуальных систем
- Год защиты: 2022
- Курс: 5
- Аннотация: В курсовой работе Зиборова Кирилла рассматривается введенная им ранее математическая модель среды исполнения смарт-контрактов и её формализация в среде интерактивного доказательства теорем HOL4. Данная модель используется для верификации смарт-контрактов, реализованных в императивном стиле на функциональном языке Standart ML. Автор показывает возможность такой реализации с помощью монадической функции монады-состояния исключения. Также, формулируются основные типы свойств, которые могут быть верифицированы с помощью построенной модели. В качестве примера представлена дедуктивная верификация в HOL4 монадических функций смарт-контракта, реализующего бизнес-логику заказа билета через туроператора. Автор доказывает теорему о связи между истинностью утверждения в состоянии смарт-контракта, выражающего некоторый статус этого состояния, и истинностью этого утверждения в последующих состояниях.
- Добавил в систему: Миронов Андрей Михайлович