Скачать plt formal methods resources - plt formal methods resources Скачать исходный код

plt formal methods resources

Другой исходный код

1.0.0

Скачать

Теория языка программирования и формальные методы — Ресурсы

Изображение Кортси: Группа Форсайтов

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

Анализ формальными методами в основном включает в себя следующие шаги:

Formal Specification
Formal Proofs
Model Checking
Abstraction

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

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

ПРИМЕЧАНИЕ :

Я постарался сделать контент более ориентированным на текущие исследования и промышленное применение. Людям, ищущим чисто академический сборник, следует обратиться к «Формальным методам в образовании» — Джереми Авигад.
Ожидается, что читатель обладает некоторыми базовыми знаниями теории типов . Более академическую информацию можно найти здесь Learn-TT.

Содержание

Книги и лекции
Блоги
МООК
Инструменты
Проекты
Предстоящие испытания
- Связанные с безопасностью
  - Безопасность программного обеспечения
  - Дифференциальная конфиденциальность
  - Приложения в области безопасности блокчейна
  - Проблемы обеспечения безопасности ИИ
  - Создавайте безопасные киберфизические системы
- Абстрактная интерпретация ориентирована
- Исследования в области языков программирования
  - Вероятностное программирование
  - Разработка языка квантового программирования
  - Совершенствование языка с использованием формальных методов
Связанные отрасли и стартапы

Книги и лекции

Основы программного обеспечения : я настоятельно рекомендую это в качестве отправного материала для более глубокого изучения этой области. Книга очень полезна для построения базовых концепций и служит хорошим введением в эту область. Красиво иллюстрированные концепции с примерами для практики представлены повсюду, что делает интерактивные теоремы, доказывающие обучение, увлекательным.
FRAP — Адам Члипала : Книга, которая поможет вам понять и обосновать формальную корректность программ. Императивный язык ( C ), вдохновленный примерами структур данных и алгоритмов, очень помогает задуматься об их формальной проверке.
Сертифицированное программирование с зависимыми типами — Адам Члипала : одна из лучших theoretical books для изучения доказательства теорем с использованием coq.
Формальная проверка – Жак Флерио : этот курс включает в себя доказательство теорем с использованием некоторых более развитых инструментов, таких как решатели SAT и SMT.
Абстрактная интерпретация - Патрик Кузо Лучший доступный материал по теории абстрактной интерпретации. Он дает полный и чистый математический анализ мутаций программы. Объясняется и доказывается поведение Программы как постоянно изменяющейся связи между различными абстрактными математическими структурами!!.
Логика и доказательство — введение в CMU и Lean : этот курс разработан в CMU и также служит вводным материалом для доказательства теорем в Lean.

Если вы чувствуете, что вам нужно больше теоретических знаний, обратитесь к примечанию выше.

Блоги

Начало работы с формальными методами
K Framework и усилия формальной проверки в блокчейне
Формальная проверка Pact для смарт-контрактов Blockchain: потрясающий короткий блог, объясняющий методологию Pact FV с небольшим введением в формальную проверку на основе основных принципов.
На пути к надежному и проверенному ИИ: тестирование спецификаций, надежное обучение и формальная проверка - DeepMind
Проблема проверки и тестирования машинного обучения - Ян Гудфеллоу и Николас Паперно

МООК

Формальная проверка программного обеспечения — edX
Количественная проверка моделей — Coursera
Киберфизические системы : курс Калифорнийского университета в Беркли, посвященный использованию методов проверки для моделирования физических систем Cyper (CPS).
Языки программирования - Coursera

Инструменты

Помощники по доказательствам

coq: Самый популярный и широко используемый инструмент для доказательства теорем. Он поддерживает множество функций, включая ML-извлечение, упаковку проектов (создание Project и Makefile). Существует множество how-to материалов, в которых для формализации используется coq. Любой может найти эти 100 теорем в Coq очень интересными.
Lean: относительно новое средство доказательства теорем от Microsoft Research . Имеет хороший интерактивный учебник, с ним легко начать.
Средство проверки моделей PRISM: средство проверки моделей, разработанное Оксфордским университетом.
Nuprl: Средство доказательства теорем Корнелла в рамках проекта логики уточнения доказательств.
Агда: Вполне зрелый помощник. Имеет функции, аналогичные Coq. легко освоить после некоторого опыта работы в coq.
Изабель: Это старый прибор для доказательства теорем. Имеет хорошую реализацию базовой логики, но не имеет других функций, связанных с UX.
VCC: механический верификатор для параллельных программ на языке C от Microsoft.
TLA+: язык высокого уровня для языков и систем моделирования (особенно параллельных и распределенных).

Решатели SAT/SMT/SMC

Решатели SAT:

МиниСат.

Решатели SMT:

Z3
CVC4
МатСАТ5
СМТИнтерпол
Принцесса

Решатели SMC:

Публикация

Гибридные решатели

Доказательные помощники имеют очень сильную реализацию программной логики. Иногда тактически невозможно провести сложные доказательства, только используя их. Поэтому текущие исследования сочетают этот принцип строгого логического рассуждения с мощными решателями SMT и SMC, чтобы облегчить разработку доказательств. Некоторые примеры приведены ниже:

Фстар(Ф*)
- Код F* можно извлечь в C с помощью KreMLin.
СМТКок

Проекты

Большинство проектов в той или иной степени являются разработкой соответствующих средств доказательства теорем или программ SAT/SMT/SMC/решателей, поэтому их можно найти там. Это некоторые из других активно разрабатываемых проектов.

DeepSpec — это зонтичный проект, направленный на создание проверенных программных систем. Активно работают над следующими крупными подпроектами:
- Компцерт
- Проверенный LLVM (VeLLVM)
- Проверенная цепочка инструментов программного обеспечения (VST)
ikos — надежный , не содержащий ошибок компилятор C, основанный на теории абстрактной интерпретации.
Project Everest: это исследовательский проект, целью которого является создание безопасной и проверенной экосистемы HTTPS.
CertiCrypt: Это проект, направленный на моделирование криптографии с открытым ключом с использованием помощника по проверке доказательств coq.
Iris: Iris — это логическая структура параллельного разделения высшего порядка, реализованная и проверенная в помощнике по доказательству Coq.
VeriDeep — проверка безопасности глубоких нейронных сетей
VeHICal: Проект направлен на разработку основ проверенного совместного проектирования интерфейсов и управления киберфизическими системами человека.
FastSMT — инструмент, который дополнит ваш решатель SMT, научившись оптимизировать его производительность для вашего набора данных формул. Он разработан лабораторией SRI ETH Zurich на базе решателя Z3 SMT.
fm4cps — Формальные методы для киберфизических систем, совместные усилия INRIA и ECNU, Шанхай.

Предстоящие испытания

Связанные с безопасностью

Безопасность программного обеспечения
- Чтения
  - Формальные методы обеспечения безопасности, семинар NSF
  - Символическая связь между формальными методами и безопасностью
  - Исследовательские документы проекта «Эверест»
  - Формальные методы в безопасности программного обеспечения
  - Формальные методы для безопасных и надежных компьютерных систем
  - Вычислительная надежность формального шифрования
  - Структуры безопасности с использованием формальных методов
  - Проверка криптографического примитива
  - Официальная сертификация криптографических доказательств на основе игр
  - Официальная сертификация криптографических доказательств на основе кода
- Видео
  - Глубокая спецификация для Dropbox
  - DSL для проверенных безопасных многосторонних вычислений в F*
  - Использование формальных методов для разработки высокозащищенных систем
  - Безопасность посредством формальных методов и безопасной архитектуры (CERIAS - Университет Пердью)
  - Языковые методы для криптографии и конфиденциальности
Дифференциальная конфиденциальность
- Чтения
  - Формальная проверка дифференциальной конфиденциальности для интерактивных систем
  - Формальные методы обеспечения конфиденциальности
  - LightDP — на пути к автоматизации дифференциальных доказательств конфиденциальности
  - EasyCrypt — проверенная дифференциальная конфиденциальность вычислений с приложениями для интеллектуальных счетчиков
  - Доказательство дифференциальной конфиденциальности в логике Хоара
  - Дифференциально частное байесовское программирование
  - Усовершенствованная вероятностная связь для дифференциальной конфиденциальности
- Видео
  - Формальные методы и доказательства свойств конфиденциальности - 1
  - Формальные методы и доказательства свойств конфиденциальности - 2
  - Формальные методы и доказательства свойств конфиденциальности - 3
  - Доказательство дифференциальной конфиденциальности с использованием реляционных типов
Приложения в области безопасности блокчейна
Формальные методы для блокчейнов : это первый семинар, посвященный использованию формальных методов в технологии блокчейн. Это будет 11 октября 2019 года .
CertiK : Это стартап, ориентированный на использование формальных методов для обеспечения проверяемой безопасности блокчейнов.
- Чтения
  - Как формальный анализ и верификация повышают безопасность систем на основе блокчейна — Учебное пособие @ MIT
  - Смарт-контракты и возможности формальных методов
  - K Framework и усилия по формальной верификации в Blockchain. Потрясающая коллекция пояснительных материалов по K framework и ее применению при проверке систем Blockchain.
  - Формальная проверка Pact для смарт-контрактов Blockchain: потрясающий короткий блог, объясняющий методологию Pact FV с небольшим введением в формальную проверку на основе основных принципов.
  - Темопоральные блокчейны – формальный анализ
  - Проверка децентрализованных смарт-контрактов с помощью теории игр и формальных методов
- Видео
  - Формальное проектирование, реализация и верификация языков блокчейна
  - CertiK — платформа формальной проверки смарт-контрактов (обзор)
  - Простота – новый язык блокчейнов
Проблемы обеспечения безопасности ИИ
FLoC 2018 — Саммит машинного обучения и формальные методы
Проверенное машинное обучение — Университет Радбауд в Неймегене : университетский курс по использованию методов проверки в машинном обучении.
Формальные методы встречаются с машинным обучением - RWTH Ахенский университет : семинар 2018 года, посвященный достижениям в области проверяемого безопасного машинного обучения с использованием формальных методов.
- Чтения
  - На пути к проверенному искусственному интеллекту - С. Сешиа
  - На пути к надежному и проверенному ИИ: тестирование спецификаций, надежное обучение и формальная проверка - DeepMind
  - Разработка систем машинного обучения без ошибок с использованием формальной математики
  - Смешение формальных методов, машинного обучения и взаимодействия человека с компьютером
  - Машинное обучение в формальных методах
  - Машинное обучение и формальные методы
  - Алгоритмы проверки глубоких нейронных сетей
  - Проверка безопасности глубоких нейронных сетей
  - Проблема проверки и тестирования машинного обучения - Ян Гудфеллоу и Николас Паперно
  - Проверка свойств бинаризованных глубоких нейронных сетей
  - Reluplex: эффективный решатель SMT для проверки глубоких нейронных сетей
  - Верификация кусочно-линейных сетей прямого распространения
  - Проблемы верификации алгоритмов обучения с подкреплением
  - Применение формальных методов в обучении с подкреплением - Galois Inc.
  - На пути к доказательству состязательной устойчивости глубоких нейронных сетей
- Видео
  - Проверка безопасности глубоких нейронных сетей – ICST 2018
  - Проверка безопасности глубоких нейронных сетей - Марта Квятковска - CAV 2017
  - Проверка безопасности глубоких нейронных сетей - INRIA
  - Правила проверки машинного обучения: от ошибок, вызванных данными, до объяснимого ИИ
  - Верификация программ машинного обучения
  - Reluplex: эффективный SMT-решатель для проверки глубоких нейронных сетей — видео конференции
  - Разработка моделей машинного обучения без ошибок с использованием Certigrad - Дэниел Селсам
Создавайте безопасные киберфизические системы
VeHICal : Проект направлен на разработку основ проверенного совместного проектирования интерфейсов и управления киберфизическими системами человека.
fm4cps — Формальные методы для киберфизических систем, совместные усилия INRIA и ECNU, Шанхай.
- Чтения
  - Проектирование киберфизических систем: формальные основы, методы и интегрированные цепочки инструментов
  - Новые рубежи формальных методов: обучение, киберфизические системы, образование и не только
  - Проверка статистической модели киберфизических систем
  - Формальная проверка транспортных киберфизических систем
  - Верификация киберфизических систем
  - Верификация и валидация в киберфизических системах: проблемы исследования и путь вперед
  - Обнаружение аномалий в киберфизических системах: подход формальных методов
  - Композиционная верификация самоадаптирующихся киберфизических систем
- Видео
  - Устав формальных методов для киберфизических систем и промышленного Интернета вещей
  - Формальная верификация киберфизических систем
  - Мониторинг киберфизических систем

Абстрактная интерпретация ориентирована

Быстрая и эффективная сертификация надежности: проект DeepZ — для сертификации надежности нейронных сетей на основе абстрактной интерпретации.
AI2: Сертификация безопасности и устойчивости нейронных сетей с абстрактной интерпретацией
Сертификация повышения надежности нейронных сетей: в своей методологии используется абстрактная интерпретация.

Связанные с исследованием языка программирования

Вероятностное программирование
- Чтения
  - Введение в вероятностное программирование
  - Формальная верификация вероятностных программ высшего порядка
  - Вероятностно-логическое программирование и байесовские сети
  - Вероятностные функции и криптографические оракулы в логике высшего порядка - Андреас Лохбихлер
  - Вероятностно-реляционная верификация криптографических реализаций
  - Доказательства связи — это вероятностные программы продуктов.
  - Усовершенствованная вероятностная связь для дифференциальной конфиденциальности
  - Формальные методы вероятностного программирования
  - Формальные методы для вероятностных программ : Слайды лекций
  - Вероятностное программирование — настоящая задача проверки
  - FairSquare: Вероятностная проверка честности программы
  - VPHL: проверенная логика частичной корректности для вероятностных программ
  - Объединение логики и вероятности
- Видео
  - Формальная верификация вероятностных программ высшего порядка – видео с конференции POPL 2019
  - Вероятностно-логическое программирование и его приложения - Люк Де Раедт, Левен
Разработка языка квантового программирования
- Чтения
  - Qwire: формальная верификация квантовых программ в Coq
  - Логика формальной верификации квантовых программ
  - Методы сопряжения для рассуждений о квантовых программах
  - Формальная верификация против квантовой неопределенности
  - Проверка модели рекурсивных квантовых протоколов
- Видео
  - Квантовые вычисления, способные выполнять миссию, для проверки и валидации программного обеспечения (VV) - CMU
  - Доминик Унру: формальная проверка квантовой криптографии
Совершенствование языков формальными методами

В частности, это касается улучшения определенных свойств (например, параллелизма и параллелизма) существующих языков программирования. По этому поводу можно легко многое узнать, поскольку, в конце концов, это единственная и самая важная причина изучать теорию PL. На всех конференциях, перечисленных здесь, ACM SIGPLAN есть большинство исследовательских работ по разработке языков программирования, их обязательно проверяют.