That was interesting - never seen Z3 applied for verification of networking and cryptographic algorithms.
My team similarly used Z3 to reverse-generate data from SQL queries so that erroneous mutations of the queries get detected early on: http://www.cse.iitb.ac.in/infolab/xdata/
Neat design! I made related a tool that crawls a given URL and generates a 3D sitemap (essentially a directed graph): https://github.com/schedutron/visualnet
Thanks for that suggestion; I'd almost forgot about that Word file! When I made this project I wasn't familiar with Git, the importance of having neat README's and heck even linting code.
I'll update the README with that file, add few explanations and instead of having those screenshots I'll try to have a gif that encapsulates a session.
Amazing work; I was wondering whether SQLancer can be integrated with systems like Cosette[1] and XData[2] in a useful way? These systems are different as in they test the "correct intention" of SQL queries and are mostly engine-agnostic.
Manual correctness checking of SQL is cumbersome and error-prone since developers may write queries in several different ways, while using fixed datasets (independent of the query) may fail to catch errors in them. XData automatically generates small datasets designed to catch errors in the queries (an example error is using a left-join instead of a full outer join).
Any ideas about how we can combine the utilities of SQLancer and XData / Cosette? I was a research intern at IITB Database Group, who developed XData and I still contribute to the project.
Built this as my high school project, in Python2. Has a neat SQL-like REPL interface. Supports auto-substitution-teacher assignment among other things. Another neat thing is that this is that there are absolutely zero third-party dependencies. Feel free to contribute as there is a BIG room for add-ons and improvement.