We present a novel symbolic reasoning engine for SQL which can efficiently generate an input I for n queries P 1 , ⋯, 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.

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).

Equivalence checking for SQL queries has many real-world applications but typically requires supporting an expressive SQL language in order to be practical. We develop VeriEQL, a system that can prove and disprove equivalence of complex SQL queries. Specifically, given two SQL queries under a database schema, VeriEQL can verify whether these two queries always produce identical results on all possible input databases up to a bounded size that conform to the schema. This paper demonstrates VeriEQL in three scenarios, including validating the correctness of query optimizations, grading SQL queries on online coding platforms, and finding implementation bugs in database management systems.

Understanding how new TCP congestion control algorithms interact with the default TCP Cubic over a wide-range of network conditions is important for moving congestion control research forward. Unfortunately, lacking are studies over actual satellite Internet networks where high latencies pose challenges to TCP performance. This paper presents results from experiments over a commercial satellite Internet link assessing TCP congestion control algorithm performance for Cubic when competing with algorithms using four different approaches: loss-based (Cubic), bandwidth-estimation based (BBR), utility function-based (PCC) and satellite optimized (Hybla). Analysis shows: 1) the default Cubic algorithms are fair to each other; 2) Cubic dominates PCC during steady state; 3) Hybla dominates Cubic during start-up; and 4) BBR dominates Cubic during both start-up and steady state.