Paper Info
Title
Demonstration of the Cosette Automated SQL Prover.
Abstract
In this demonstration, we showcase COSETTE, the first automated prover for determining the equivalences of SQL queries. Despite theoretical limitations, COSETTE leverages recent advances in both automated constraint solving and interactive theorem proving to decide the equivalences of a wide range of real world queries, including complex rewrite rules from the database literature. COSETTE can also validate the inequality of queries by finding counter examples, i.e., database instances which, when executed on the two queries, will return different results. COSETTE can find counter examples of many real world inequivalent queries including a number of real-world optimizer bugs. We showcase three representative applications of COSETTE: proving a query rewrite rule from magic set rewrite, finding counter examples from the infamous optimizer bug, and an interactive visualization of automated grading results powered by COSETTE, where COSETTE is used to check the equivalence of students' answers to the standard solution. For the demo, the audience can experience through the three applications, and explore the COSETTE by interacting with the tool using an easy-to-use web interface.
Year
DOI
Venue
2017
10.1145/3035918.3058728
SIGMOD Conference
Field
DocType
Citations 
Data mining,Programming language,Computer science,Correctness,Theoretical computer science,Equivalence (measure theory),Gas meter prover,SQL,Interactive visualization,Counterexample,User interface,Database,Proof assistant
Conference
2
PageRank 
References 
Authors
0.42
10
5
Name
Order
Citations
PageRank
Shumo Chu129711.08
Daniel Li220.42
Chenglong Wang3857.26
Alvin Cheung446636.20
Dan Suciu596251349.54