Город: Санкт-Петербург Новосибирск Казань Язык: Русский English

Введение в формальную верификацию программ
Санкт-Петербург / весна 2021, посмотреть все семестры

Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

О чем курс

Формальная верификация программ — это набор парадигм, техник и инструментов, гарантирующих с той или иной степенью надёжности корректность программ. Думаю многие согласятся, что есть области ИТ, в которых корректность заслуживает самого пристального внимания: прошивки бортовых компьютеров самолетов, автомобилей, кардиостимуляторов, софт атомных электростанций и др.

Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем Coq (https://coq.inria.fr), теория типов, лежащей в ее основе, метапрограммирование в Coq и применение Coq к верификации функциональных алгоритмов.

Лекции будут читаться через zoom. Ссылка для подключения будет опубликована в новостях курса (её получат те, кто запишется на курс).

Материалы к курсу

По мере прохождения курса материалы будут выкладываться в репозитории по адресу: https://github.com/anton-trunov/csclub-coq-course-spring-2021.

Пререквизиты к курсу

  • Базовое функциональное программирование (анонимные функции, рекурсия, функции высшего порядка, алгебраические типы данных, паттерн-матчинг)
  • Классическая (или интуиционистская) логика высказываний и логика предикатов.

Программа курса

  1. Введение в курс, основы тотального функционального программирования в Coq, интерактивные запросы в Coq
  2. Алгебраические типы данных, элементы соответствия Карри-Говарда, интуиционистская пропозициональная логика. Зависимые типы и зависимый паттерн-матчинг, пропозициональное равенство, инъективность и дизъюнктивность конструкторов.
  3. Кванторы всеобщности и существования. Доказательства по индукции. Индукция и рекурсия.
  4. Язык тактик SSReflect. Виды индукции: математическая, парная, сильная. Эвристики для доказательств по индукции. Списки. Структурная индукция для списков.
  5. Разрешимые свойства, reflect-предикат, виды и подсказки видов, спецификации и зависимые типы, коэрции.
  6. Анализ случаев для семейств типов. adhoc полиморфизм и канонические структуры. Архитектура типа с равенством (eqType). Канонические миксины. Фантомные типы. Клонирующие конструкторы. Унификация и η-расширение.
  7. Подтипирование. Неразличимость доказательств. Конечные типы, ординалы, кортежи.
  8. Prop и Type. Непредикативность Prop, предикативность Type. Большая элиминация и закон исключенного третьего. Тотальность и завершаемость программ. Плагины Function, Program, Equations. Правило строгой позитивности для индуктивных типов. Полиморфизм по уровням вселенных. Парадокс Рассела в Coq.
  9. Спецификация и верификация функциональных алгоритмов. Индуктивные предикаты. Деревья Брауна: подходы к реализации. Экстракция.
  10. Рандомизированное тестирование свойств (QuickChick). Мутационное тестирование доказательств. Автоматизация доказательств: встроенные тактики, интеграция SMT-решателей в Coq, использование технологий, построенных на машинном обучении.

Пожалуйста, обратите внимание, что программа курса примерная и перечень тем, а также глубина их рассмотрения может корректироваться по ходу курса.

Чат курса

Телеграм: https://t.me/joinchat/Ge1_yrqEFxEzYjAy. В чате можно попросить помощи с инсталляцией (см. ниже), что-то уточнить, обсудить домашние задания, указать на ошибки/опечатки и т.п.

Базовая литература

Полезные ссылки

Программное обеспечение для семинаров/практических занятий

Вам будет нужен компьютер со следующим установленным программным обеспечением

  • Coq версии 8.13 (текущий патч-релиз на момент написания -- 8.13.1)
  • библиотека Mathcomp версии 1.12.0
  • одна из интерактивных сред для редактирования доказательств: CoqIDE или VsCoq (плагин для VSCode -- рекомендуется для начинающих) или Proof General (мод для Emacs). Cреда для редактирования может быть любой относительно недавней версии.

Важно: без интерактивной среды взаимодействие с Coq сильно усложняется. Если вы очень не любите среды для редактирования, то можно использовать интерпретатор coqtop, входящий в комплект поставки Coq.

Где прочитать про установку

В настоящий момент рекомендуемый способ установить Coq на Linux и Windows -- это воспользоваться Coq Platform, помимо Coq включающей в себя большое количество предустановленных библиотек. Про этот способ установки можно прочитать в wiki: https://github.com/coq/coq/wiki#coq-installation.

Если вам нужна помощь с установкой, то, пожалуйста, обратитесь в чат курса до первого занятия (Телеграм: https://t.me/joinchat/Ge1_yrqEFxEzYjAy) -- установка может занять достаточно много времени (иногда требуется компиляция из исходников).

Как понять, что все установилось правильно

В интерактивной среде по вашему выбору введите

From mathcomp Require Import ssreflect.

и выполните команду сделать шаг или проверить весь файл. В результате может появиться много предупреждений, но не должно быть ошибки вида

Error: Unable to locate library
ssreflect with prefix mathcomp. (While searching for a .vos file.)

Запасные варианты

  • JsCoq Interactive Online System -- можно запустить Coq в браузере. Чтобы запустить JsCoq с пустым файлом воспользуйтесь следующей ссылкой: https://coq-next.vercel.app/scratchpad.html. Внимание: версии Coq и Mathcomp могут отличаться от используемых в курсе.
Дата и время Занятие Место Материалы
11 марта
22:30–00:00
Введение в курс, основы функционального программирования в Coq, Лекция Конференция в zoom, Онлайн видео,  другое
12 марта
00:30–01:30
Основы функционального программирования в Coq (продолжение 1й лекции), Семинар Конференция в zoom, Онлайн Нет
18 марта
22:30–00:00
Полиморфные функции, зависимые функции, тип-произведение, тип-сумма, неявные аргументы, нотации, Лекция Конференция в zoom, Онлайн видео
19 марта
00:30–01:30
Упражнения на тип-произведение, тип-сумму, пустой тип и единичный тип, Семинар Конференция в zoom, Онлайн
25 марта
22:30–00:00
Интуиционистская логика, определение логических связок внутри Coq, равенство, зависимый паттерн-матчинг, Лекция Конференция в zoom, Онлайн видео
26 марта
00:30–01:30
Доказательства интуиционистских высказываний через явное выписывание термов, упражнения на зависимый паттерн-матчинг, Семинар Конференция в zoom, Онлайн
01 апреля
22:30–00:00
Инъективность и дизъюнктность конструкторов. Большая элиминация. Паттерн "конвой". Доказательства по индукции. Prop и Type., Лекция Конференция в zoom, Онлайн видео
02 апреля
00:30–01:30
Упражнения на зависимый паттерн-матчинг по теме лекции 4, Семинар Конференция в zoom, Онлайн
08 апреля
22:30–00:00
Язык тактик SSReflect, Лекция Конференция в zoom, Онлайн видео
09 апреля
00:30–01:30
Практикум по языку тактик SSReflect, Семинар Конференция в zoom, Онлайн
15 апреля
22:30–00:00
Техники доказательств по индукции. Основные идеи методологии доказательств через маломасштабную рефлексию., Лекция Конференция в zoom, Онлайн видео
16 апреля
00:30–01:30
Практикум по индуктивным доказательствам, Семинар Конференция в zoom, Онлайн
22 апреля
22:30–00:00
reflect-предикат, мульти-правила переписывания, Лекция Конференция в zoom, Онлайн видео
23 апреля
00:30–01:30
Практикум по применению reflect-предикатов и мульти-правил переписывания, Семинар Конференция в zoom, Онлайн
29 апреля
22:30–00:00
Канонические структуры. Построение иерархий., Лекция Конференция в zoom, Онлайн видео
30 апреля
00:30–01:30
Построение инстансов типа с разрешимым равенством. Метапрограммирование с каноническими структурами, Семинар Конференция в zoom, Онлайн
13 мая
22:30–00:00
Верификация сортировки вставками и слиянием. Рекурсивные функции с неструктурной рекурсией. Плагин Program. Acc-предикат и рекурсивные функции., Лекция Конференция в zoom, Онлайн видео
14 мая
00:30–01:30
Верификация сортировки вставками. Реализация рекурсивных функций с неструктурной рекурсией., Семинар Конференция в zoom, Онлайн
20 мая
22:30–00:00
Автоматизация доказательств (линейная целочисленная арифметика, интеграция с решателями), плагин Equations, рандомизированное тестирование, мутационные техники, экстракция, Лекция Конференция в zoom, Онлайн видео
21 мая
00:30–01:30
Доказательства на разные темы, разбор необходимости проверок структурной рекурсии, строгой позитивности, исключение Type:Type, Семинар Конференция в zoom, Онлайн Нет