ruSTEP17mar22UshakovaMS

Мария Сергеевна Ушакова (Сибирский Федеральный Университет, Красноярск): Формальная верификация функционально-потоковых параллельных программ.
Аннотация: Доклад посвящен использованию методов формальной верификации для программ, разрабатываемых на языке Пифагор. Лежащая в основе языка функционально-потоковая модель параллельных вычислений позволяет представлять программу в виде информационного графа, не связанного ресурсными ограничениями. Это позволяет при формальной верификации ориентироваться только на логику информационных зависимостей программы, упрощая тем самым процесс анализа. В рамках проделанных исследований для функционально-потоковых параллельных программ разработан метод формальной верификации, основанный на исчислении Хоара. Для повышения наглядности при проведении доказательства используется визуальное представление информационного графа программы. Также для лучшего понимания функционально-потоковой парадигмы параллельного программирования в докладе будет кратко охарактеризован весь проект Пифагор.
Доклад представляет материалам и результаты кандидатской диссертации по специальности 2.3.5. - Математическое и программное обеспечение вычислительных систем, комплексов и компьютерных сетей (технические науки). С текстом диссертации и авторефератом можно познакомиться по ссылке https://research.sfu-kras.ru/node/14728.