[12.12.2024] QED: A Powerful Query Equivalence Decider for SQL

[Ruslan Savchenko]

Сегодня в 16:30 состоится доклад Чуркина Алексея QED: A Powerful Query Equivalence Decider for SQL

Аннотация

Посмотрим на основные способы проверки SQL запросов на эквивалентность.  Узнаем что такое bag-семантика для SQL запросов, при чем здесь лямбда термы, как можно свести SQL запрос к структуре объектов на полукольцах. После чего познакомимся с имеющимися способами для доказательства эквивалентности: различные rewrite-ы для приведения к нормальной форме (SPES), формальное доказательство на языке Coq (Cosette).

В статье QED авторы предлагают новый подход, который разберем детально: сведение запросов к логической формуле первого порядка, а задачу эквивалентности запросов к задаче эквивалентности SMT формул. Этот подход позволяет обойти в 2 раза state of the art, SPES, по количеству найденных эквивалентных запросов.

[Ruslan Savchenko]

Уже начинаем https://yandex.zoom.us/j/91482099342

--

Best regards,
Ruslan Savchenko

[Ruslan Savchenko]

Запись https://disk.yandex.ru/i/ymE0WoCH8t4-oA