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

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