Буренков Владимир Сергеевич

Рассматриваются методы верификации протоколов когерентности памяти, применяемых в многоядерных системах с разделяемой памятью. Представляются методы, основанные на model checking и на доказательстве теорем. Анализируются границы применимости данных методов. Для параметризованной верификации протоколов когерентности обосновывается необходимость методов, базирующихся одновременно как на model checking, так и на доказательстве теорем. Ключевыми аспектами таких методов является способ абстракции исходной модели протокола, а также алгоритм модификации абстрактной модели с целью устранения ложных контрпримеров.