Cosette
SQL equivalence solver
An automated solver for SQL equivalences, leveraging Coq and Lean for formal verification.
Cosette is an automated SQL solver.
666 stars
43 watching
54 forks
Language: Lean
last commit: almost 3 years ago
Linked from 2 awesome lists
coqdatabaserosettesqlverification
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 acorrenson/saturne | A verified SAT solver with proof capabilities | 28 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 uds-psl/autosubst2 | A tool for generating Coq code from syntactic theories with variable binders | 17 |
 coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 lysxia/advent-of-coq-2018 | Formally verifying and implementing solutions to Advent of Code 2018 challenges in Coq | 140 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 affeldt-aist/monae | A Coq library for formalizing and reasoning about monads with equational logic | 68 |
 meithecatte/busycoq | A project providing verified implementations of Busy Beaver deciders using Coq proof and verification. | 39 |
| uds-psl/coq-library-undecidability | A collection of mechanized undecidability proofs in Coq | 111 |
 sqlancer/sqlancer | Automated testing tool to identify logic and performance issues in databases | 1,498 |