Исследовательская группа

Лаборатория языковых инструментов

Применение SAT-солверов для проверки аксиоматических моделей памяти

May 14

Современные модели памяти сложны, что приводит к необходимости иметь автоматические средства их проверки. В докладе на примере одного из таких инструментов [1] будет рассмотрен способ проверки моделей памяти с помощью сведения к SAT. Сведение происходит через реляционную логику, в которой кодируются модели памяти. Акцент в докладе будет сделан на модели памяти Java.

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

Материалы к докладу:

Torlak, Emina, Mandana Vaziri, and Julian Dolby. "MemSAT: checking axiomatic specifications of memory models." In ACM Sigplan Notices, vol. 45, no. 6, pp. 341-350. ACM, 2010.

Докладчик: Дмитрий Суворов, Университет ИТМО