Formal verification of functional dataflow parallel programs is considered. Errors that are typical for imperative parallel programs are entirely absent in functional dataflow parallel programs. As a result, formal verification of such programs is easier. The correctness of an example program in Pifagor language is analyzed.

Рассматривается формальная верификация функционально-потоковых параллельных программ. Ошибки, характерные для императивных параллельных программ, отсутствуют в функционально-потоковых параллельных программах, что позволяет упростить верификацию. Анализируется корректность примера программы на языке Пифагор.