PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Fri 20 Jun 2025 14:40 - 15:00 at Grand Ball Room 1 - Databases

This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitable notion of equivalence in this setting, we introduce the concept of database transformers, which transform database instances between graph and relational models. We then propose a novel verification methodology that checks equivalence modulo a given transformer by reducing the original problem to verifying equivalence between a pair of SQL queries. This reduction is achieved by embedding a subset of Cypher into SQL through syntax-directed translation, allowing us to leverage existing research on automated reasoning for SQL while obviating the need for reasoning simultaneously over two different data models. We have implemented our approach in a tool called Graphiti and used it to check equivalence between graph and relational queries. Our experiments demonstrate that Graphiti is useful both for verification and refutation and that it can uncover subtle bugs, including those found in Cypher tutorials and academic papers.

This program is tentative and subject to change.

Fri 20 Jun

Displayed time zone: Seoul change

14:00 - 15:20
14:00
20m
Talk
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
PLDI Research Papers
Pinhan Zhao University of Michigan, Yuepeng Wang Simon Fraser University, Xinyu Wang University of Michigan
DOI Pre-print
14:20
20m
Talk
Pointer Analysis for Database-Backed Applications
PLDI Research Papers
Yufei Liang Nanjing University, Teng Zhang Nanjing University, Ganlin Li Nanjing University, Tian Tan Nanjing University, Chang Xu Nanjing University, Chun Cao Nanjing University, Xiaoxing Ma Nanjing University, Yue Li Nanjing University
DOI
14:40
20m
Talk
Graphiti: Bridging Graph and Relational Database Queries
PLDI Research Papers
Yang He Simon Fraser University, Ruijie Fang University of Texas at Austin, Işıl Dillig University of Texas at Austin, Yuepeng Wang Simon Fraser University
DOI
15:00
20m
Talk
AWDIT: An Optimal Weak Database Isolation Tester
PLDI Research Papers
Lasse Møldrup Aarhus University, Andreas Pavlogiannis Aarhus University
DOI