Аннотация доклада.

В докладе рассматриваются вопросы построения формальной семантики параллельных программ с использованием общего подхода к формальной верификации программ на базе λ-исчисления с зависимыми типами и с использованием предметно-ориентированных языков. В рамках этого подхода представлена модификация построенной ранее модели динамического параллельного исполнения программ, которая допускает описание ограниченного класса программ с глобальным изменяемым состоянием.