Тип публикации: патент
Год издания: 2021
Аннотация: Программа предназначена для поддержки процесса формальной верификации функционально-потоковых параллельных программ на языке Пифагор. Программа позволяет осуществлять формальную верификацию программ на основе исчисления Хоара в следующем порядке: программа загружается в виде реверсивного информационного графа, для которого осуществПоказать полностьюляется построение дерева доказательства; информационный граф изменяется, его дуги размечаются формулами на языке спецификации с использованием теорем для функций с доказанной корректностью, хранящихся в библиотеке; после получения полностью размеченного графа генерируются условия корректности на языке спецификации; программа с доказанной корректностью заносится в библиотеку и используется в последующих доказательствах. Программа может быть использована разработчиками параллельного ПО в различных областях науки и техники. Тип ЭВМ: IBM PC-совмест. ПК на базе процессоров Intel; ОС: Linux.