Tool Description and Publications

I have developed and benchmarked a tool performing symbolic execution of Java methods with embedded SQL statements. The principles behind this tool can be found in our SCP paper.

This tool is only a research prototype, its development has sadly been abandoned since 2013 and I cannot provide any kind support for it. It is written in Java and relies on the Z3 SMT solver as a backend. You can reuse the tool, code and benchmarks (for non-commercial purposes only) if you wish, but you must then appropriately cite our SCP paper.

The tool receives a SimpleDB (.sdb or .esdb) file as input, containing the SQL schema of a relational database, as well as the code of a Java method interacting with this database through SQL statements. SimpleDB files only support a core and normalised subset of SQL, together with a minimal number of imperative Java constructs (these exact subsets are detailed in the SCP paper).

The tool performs (statically) a symbolic execution of the Java method, according to the principles detailed in the SCP paper (this execution could be coupled with a concrete execution, as dynamic symbolic execution tools do. See our CSTVA paper about this and other desirable extensions). The tool generates an XML file as output, listing notably all the explored execution paths, with the corresponding test inputs (including valid database content) for the feasible ones.

Downloads

You can download the tool and benchmarks: source code - benchmarks.