Методы Флойда
Учебное пособие по методам Флойда — http://mfsp.cmc.msu.ru/w/wp-content/uploads/2015/07/Deductive-Verification-Practicum.pdf
Опечатки в печатной версии пособия — http://mfsp.cmc.msu.ru/w/?page_id=80
Учебное пособие «Введение в формальные методы верификации программ» — http://sp.cs.msu.ru/courses/vmp/kamkin_mc2018.pdf
PVS
Сайт системы PVS — http://pvs.csl.sri.com/
Виртуальная машина VirtualBox с установленной системой PVS — http://pvs.csl.sri.com/cgi-bin/downloadlic.cgi?file=NASA-NIA_PVS_Class_2012.vdi.zip
Документация по системе PVS — http://pvs.csl.sri.com/documentation.shtml : язык спецификации PVS описан в документе Language Reference, команды прувера PVS описаны в документе Prover Guide
PyFloyd
Проект PyFloyd — адрес git-репозитория https://github.com/kornevgen/floyd , далее tools/pyfloyd
Why3
Страница проекта Why3 — http://why3.lri.fr/. Там же есть ссылки на солверы.
Описание языка Why3 и инструментария — http://why3.lri.fr/manual.pdf.
Инструкция по установке — смотрите ниже ссылку на инструкцию по установке Frama-C + Jessie из проекта Astraver.
ACSL
ACSL Language Reference (последняя версия) — https://frama-c.com/download/acsl.pdf
ACSL Mini Tutorial — https://frama-c.com/download/acsl-tutorial.pdf
ACSL by example — https://github.com/fraunhoferfokus/acsl-by-example
Frama-C + Jessie @ ISPRAS
Виртуальная машина VirtualBox с Frama-C — https://yadi.sk/d/L1HQFpGq3TqHpf
Проект ИСП РАН Astraver — http://astraver.linuxtesting.org/
Инструкция по установке Frama-C + Jessie из проекта Astraver — http://astraver.linuxtesting.org/manuals/setup/
ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver — http://frama-c.com/download/acsl-implementation-Sodium-20150201.pdf
Jessie Plugin — http://krakatoa.lri.fr/jessie.pdf
Jessie Tutorial — https://frama-c.com/jessie/jessie-tutorial.pdf