SANER 2025 release

The benchmark artefact for the SANER 2025 paper "StriCT-BJ: A String Constraint Benchmark from Real Java Programs".

dataset artefact

Dataset artefact

The dataset is uploaded to the release of this repository.

The dataset is an archive folder and every folder under it contains a .jar file that contains the corresponding bytecode of a Java project (usually downloaded from Maven repository), a smt folder that contains .smt2 SMT-LIB scripts, and a simple_statistics.json file that contains statistics.

The statistics are collected with Python scripts, and every entry corresponds to a .smt2 script. Solvers are tested on the script and their performances are recorded in the statistics.

The SMT-LIB scripts and the statistics are referred to as "the full dataset", as opposed to "the thin dataset" whose entries are selected with the Python statement item["undefined_function_count"] < 1 and len(item["api_count"]) > 0 from the simple_statistics.json file.

example workflow

Take a sample file called ICUTransformFilter.java, transform it using soot-parse-text branch (using a hard-coded jar file now, which is from maven repo and may be built from a different source from the github source) into a .cpath file and output using a private peer-built path checker to .output.