Шаблон:Current Seminars — различия между версиями

Рассматриваются задачи верификация одного класса систем взаимодействующих процессов с конечным числом состояний, которые обмениваются данными с помощью неограниченных ненадежных FIFO каналов с возможностью потери сообщений. Показано, что для этого класса распределенных систем разрешимы некоторые задачи верификации, а именно проблемы достижимости, проблема безопасности относительно регулярных множеств трасс и проблемы живости относительно множеств состояний управления. При этом следует заметить (и это очень удивительно!), что 1) все перечисленные задачи алгоритмически неразрешимы в том случае, если для каналы абсолютно надежны и 2) сложность указанных задач неэлементарна.

равенствами.

В докладе рассматривается метод преобразования программ на нестрогом функциональном языке первого порядка, основанный на комбинации методов насыщения равенствами и суперкомпиляции. Общая идея метода совпадает с идеей насыщения равенствами (предложенного в работе "Equality Saturation: A New Approach to Optimization" Тейта и др. для преобразования императивных программ) и заключается в преобразовании структуры данных, описывающей целое множество программ, а не одну программу. Используемые преобразования, однако, в основном взяты из суперкомпиляции. В рамках метода также предложено преобразование, названное слиянием по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Показано, что метод применим для индуктивного доказательства эквивалентности программ.