Инструментальное средство для формальной верификации функционально-потоковых параллельных программ на языке Пифагор на основе исчисления Хоара : регистрация программы для ЭВМ | Научно-инновационный портал СФУ

Инструментальное средство для формальной верификации функционально-потоковых параллельных программ на языке Пифагор на основе исчисления Хоара : регистрация программы для ЭВМ

Тип публикации: патент

Год издания: 2021

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

Ссылки на полный текст

Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.