Q*cert       

links

 Louis Mandel photo Avraham E (Avi) Shinnar photoJerome Simeon photo

Q*cert - overview


Q*cert is a query compiler written using the Coq proof assistant and a platform for implementing and verifying query compilers.

Data processing is central to modern applications, and guaranteeing the correctness of consistency of the data is important. Q*cert leverages recent advances in theorem proving technology to provide correctness guarantees for the query compiler, including its optimizers.

Q*cert is an open-source project, and its source code and documentation is available on github at https://querycert.github.io