Cosette

Tech stack & purpose

Cosette is an automated solver for reasoning about SQL equivalences, implemented as a domain-specific language that can verify whether two SQL queries are semantically equivalent. The project is built using Haskell for its parser and core DSL components, and generates code for both the Rosette solver and the Coq proof assistant to perform formal verification. The work is from the University of Washington database group (uwdb), though the repository is now deprecated in favor of a successor project called QED.

Community & reference links

• cosette.cs.washington.edu/
• the Cosette Guide
• demo.cosette.cs.washington.edu/
• gitter.im/uwdb/Cosette
• Introducing Cosette

Languages

Contributors

• 
  Shumo Chu350 commits · 221 followers
• 
  Chenglong Wang64 commits · 60 followers
• 
  Shumo Chu61 commits · 221 followers
• 
  Brendan Seamas Murphy41 commits · 41 followers
• Konstantin Weitz9 commits
• Daniel Li5 commits
• 
  Alvin Cheung4 commits · 66 followers
• 
  Jared Roesch3 commits · 410 followers
• clwang2 commits
• 
  Toni Müller1 commits · 15 followers
• 
  Chenglong Wang1 commits · 60 followers
• Brant Fitzsimmons1 commits