VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity ConstraintsOOPSLA 2024 Distinguished Paper Award
This program is tentative and subject to change.
The task of SQL query equivalence checking is important in various real-world applications (including query rewriting and automated grading) that involve complex queries with integrity constraints; yet, state-of-the-art techniques are very limited in their capability of reasoning about complex features (e.g., those that involve sorting, case statement, rich integrity constraints, etc.) in real-life queries. To the best of our knowledge, we propose the first SMT-based approach and its implementation, VeriEQL, capable of proving and disproving bounded equivalence of complex SQL queries. VeriEQL is based on a new logical encoding that models query semantics over symbolic tuples using the theory of integers with uninterpreted functions. It is simple yet highly practical — our comprehensive evaluation on over 20,000 benchmarks shows that VeriEQL outperforms all state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be proved or disproved. VeriEQL can also generate counterexamples that facilitate many downstream tasks (such as finding serious bugs in systems like MySQL and Apache Calcite).
This program is tentative and subject to change.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | Static Analysis and Program Verification 3OOPSLA 2024 at IBR East Chair(s): Frank Tip Northeastern University | ||
16:00 20mTalk | Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach OOPSLA 2024 Haonan Li University of California at Riverside, USA, Yu Hao University of California at Riverside, USA, Yizhuo Zhai University of California at Riverside, USA, Zhiyun Qian University of California at Riverside, USA | ||
16:20 20mTalk | PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis OOPSLA 2024 Zhaoyu Wang HKUST, Pingchuan Ma HKUST, Huaijin Wang , Shuai Wang Hong Kong University of Science and Technology | ||
16:40 20mTalk | Semantic-Type-Guided Bug Finding OOPSLA 2024 Kelvin Qian Johns Hopkins University, Scott F. Smith The Johns Hopkins University, Brandon Stride Johns Hopkins University, Shiwei Weng Johns Hopkins University, Ke Wu Johns Hopkins University DOI | ||
17:00 20mTalk | Seneca: Taint-Based Call Graph Construction for Java Object Deserialization OOPSLA 2024 Joanna C. S. Santos University of Notre Dame, Mehdi Mirakhorli Rochester Institute of Technology, Ali Shokri Virginia Tech | ||
17:20 20mTalk | VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity ConstraintsOOPSLA 2024 Distinguished Paper Award OOPSLA 2024 Yang He Simon Fraser University, Pinhan Zhao University of Michigan, Xinyu Wang University of Michigan, Yuepeng Wang Simon Fraser University DOI Pre-print |