The XData project[1] at IIT Bombay is an interesting use case. The problem is to figure out whether the query a student wrote is semantically equivalent to that

The XData project[1] at IIT Bombay is an interesting use case. The problem is to figure out whether the query a student wrote is semantically equivalent to that written by the professor. There is too much variation and many syntactic differences between different databases to do equivalence testing using just syntax analysis. Instead, Z3 is used to generate a small test data set, given the schema and the query. The core idea is to make sure the data set smokes out any mutation to the query. That is, if I use a join when the prof intended outer join to be used, or '<" instead of '<=', Z3 is used to generate a data set that will yield different results for the original and mutated queries. Once a sufficiently robust data set is created that covers (an extensive list of) common errors, it can be used to vet student queries automatically. Interestingly, the system can award partial marks as well. [1] https://www.cse.iitb.ac.in/infolab/xdata/ https://www.cse.iitb.ac.in/infolab/xdata/