Теоретические материалы

Методы Флойда

Учебное пособие по методам Флойда — 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

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://cdn0.scrvt.com/fokus/c8efcdaac330d718/6cc5d3fc9481/ACSL-by-Example_14_1_0.pdf

Frama-C + Jessie

Виртуальная машина 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