This program is tentative and subject to change.

Wed 23 Oct 2024 17:20 - 17:40 at IBR East - Static Analysis and Program Verification 3 Chair(s): Frank Tip

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 Oct

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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