Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
This program is tentative and subject to change.
We present a novel symbolic reasoning engine for SQL which can efficiently generate an input $I$ for $n$ queries $P_1, \cdots, P_n$, such that their outputs on $I$ satisfy a given property (expressed in SMT). This is useful in different contexts, such as disproving equivalence of two SQL queries and disambiguating a set of queries. Our first idea is to reason about an under-approximation of each $P_i$ — that is, a subset of $P_i$'s input-output behaviors. While it makes our approach both semantics-aware and lightweight, this idea alone is incomplete (as a fixed under-approximation might miss some behaviors of interest). Therefore, our second idea is to perform search over an expressive family of under-approximations (which collectively cover all program behaviors of interest), thereby making our approach complete. We have implemented these ideas in a tool, Polygon, and evaluated it on over 30,000 benchmarks across two tasks (namely, SQL equivalence refutation and query disambiguation). Our evaluation results show that Polygon significantly outperforms all prior techniques.
This program is tentative and subject to change.
Fri 20 JunDisplayed time zone: Seoul change
14:00 - 15:20 | |||
14:00 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | AWDIT: An Optimal Weak Database Isolation Tester PLDI Research Papers DOI |