Introducing Cosette

What is a SQL solver and what can it do?

  1. If the two SQL queries are equivalent, Cosette will find a mechanical proof for the equivalence and validate it in using a Proof Assistant (currently Coq).
  2. If the two SQL queries are inequivalent, Cosette will find a counterexample to show they are not equivalent. A counterexample is a set of specific input relation(s), where the two SQL queries will produce different results when executed using them, such as the one shown above.

Proving equivalences of SQL queries

Finding counterexamples

Learn and Use Cosette




Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Intro to Apache Spark from O’Reilly Learning Spark (Summary)

How to understand and develop a Nmap of your Own — Part 2 — CyberForged

Double Eleven Technology Series: Logistics and Dynamic Path Planning

Things to keep in mind when take input from user.

Waterfall vs Agile: Is It Still Worth Asking?

Spring boot-camunda-Configuration

AWS S3 in Elixir with ExAws

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
University of Washington Database Group

University of Washington Database Group

More from Medium

Setting Up Spark Environment

I have not been a fan of adventure cameras because I have no need for them because I don’t do…

CI/CD of Machine Learning Models using ML-Flow

Trigger AWS Lambda from Amazon SQS