City: Test Saint Petersburg Novosibirsk Kazan Language: Русский English

Introduction to Formal Verification
Saint Petersburg / spring 2021, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

О чем курс

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

Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем 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 могут отличаться от используемых в курсе.
Date and time Class|Name Venue|short Materials
11 March
22:30–00:00
Введение в курс, основы функционального программирования в Coq, Lecture Конференция в zoom, Онлайн video,  other
12 March
00:30–01:30
Основы функционального программирования в Coq (продолжение 1й лекции), Seminar Конференция в zoom, Онлайн No
18 March
22:30–00:00
Полиморфные функции, зависимые функции, тип-произведение, тип-сумма, неявные аргументы, нотации, Lecture Конференция в zoom, Онлайн video
19 March
00:30–01:30
Упражнения на тип-произведение, тип-сумму, пустой тип и единичный тип, Seminar Конференция в zoom, Онлайн
25 March
22:30–00:00
Интуиционистская логика, определение логических связок внутри Coq, равенство, зависимый паттерн-матчинг, Lecture Конференция в zoom, Онлайн video
26 March
00:30–01:30
Доказательства интуиционистских высказываний через явное выписывание термов, упражнения на зависимый паттерн-матчинг, Seminar Конференция в zoom, Онлайн
01 April
22:30–00:00
Инъективность и дизъюнктность конструкторов. Большая элиминация. Паттерн "конвой". Доказательства по индукции. Prop и Type., Lecture Конференция в zoom, Онлайн video
02 April
00:30–01:30
Упражнения на зависимый паттерн-матчинг по теме лекции 4, Seminar Конференция в zoom, Онлайн
08 April
22:30–00:00
Язык тактик SSReflect, Lecture Конференция в zoom, Онлайн video
09 April
00:30–01:30
Практикум по языку тактик SSReflect, Seminar Конференция в zoom, Онлайн
15 April
22:30–00:00
Техники доказательств по индукции. Основные идеи методологии доказательств через маломасштабную рефлексию., Lecture Конференция в zoom, Онлайн video
16 April
00:30–01:30
Практикум по индуктивным доказательствам, Seminar Конференция в zoom, Онлайн
22 April
22:30–00:00
reflect-предикат, мульти-правила переписывания, Lecture Конференция в zoom, Онлайн video
23 April
00:30–01:30
Практикум по применению reflect-предикатов и мульти-правил переписывания, Seminar Конференция в zoom, Онлайн
29 April
22:30–00:00
Канонические структуры. Построение иерархий., Lecture Конференция в zoom, Онлайн video
30 April
00:30–01:30
Построение инстансов типа с разрешимым равенством. Метапрограммирование с каноническими структурами, Seminar Конференция в zoom, Онлайн
13 May
22:30–00:00
Верификация сортировки вставками и слиянием. Рекурсивные функции с неструктурной рекурсией. Плагин Program. Acc-предикат и рекурсивные функции., Lecture Конференция в zoom, Онлайн video
14 May
00:30–01:30
Верификация сортировки вставками. Реализация рекурсивных функций с неструктурной рекурсией., Seminar Конференция в zoom, Онлайн
20 May
22:30–00:00
Автоматизация доказательств (линейная целочисленная арифметика, интеграция с решателями), плагин Equations, рандомизированное тестирование, мутационные техники, экстракция, Lecture Конференция в zoom, Онлайн video
21 May
00:30–01:30
Доказательства на разные темы, разбор необходимости проверок структурной рекурсии, строгой позитивности, исключение Type:Type, Seminar Конференция в zoom, Онлайн No