weakmemory.github.io

Формальные методы дизайна и верификации программного обеспечения: семантики языков программирования

• Инструкция по настройке окружения
• Репозиторий с вводными задачами по Coq. Пройдите по ссылке, чтобы создать свою копию репозитория.
• Репозиторий с задачами по семантикам. Приступайте к этим задачам после того, как закончите предыдущие. В этом репозитории решайте задачи в файлах Id.v, State.v, Expr.v, Stmt.v и Hoare.v.

Задания для знакомых с Coq:

1. Доказать существование отсортированной перестановки списка так, чтобы при экстракции получался Mergesort.
2. Доказать полноту исчисления резолюций.

Задания для знакомых с Coq и семантиками:

1. Реализовать операционную модель x86+FPGA из статьи Iorga-al:OOPSLA21.

По всем вопросам обращайтесь к Антону и Егору