The Basic Expeirmental Benchmark for Dependence Guided Symbolic Execution

This benchmark consists of all nine programs in our experiments of the paper titled dependence guided symbolic execution, of which there are five programs from Siemens Suite, WBS, Siena, Apache CLI and NanoXML.

The benchmark can be downloaded here, and further details are described in the Readme file contained in the downloaded package.

The Benchmark for Mutation Testing

This benchmark consists of the mutants of the six programs, which are used in our mutation testing experiments of the paper titled dependence guided symbolic execution. The six programs consist of five programs from Siemens Suite and WBS. The Siemens Suite is specially designed to evaluate the fault detection capabilities of control-flow and data-flow coverage criteria. Besides, we add the WBS into the benchmark, which is distributed with Symbolic PathFinder tool. The mutants of this benchmark are automatically generated by the mutation testing tool muJava. The procedures how to automatically generate the mutants can refer to muJava.

The benchmark can be downloaded here, and further details are described in the Readme file contained in the downloaded package.

The Prototype Tools of Dependence Guided Symbolic Execution

The experimental tools contain three projects, which are STVRDepen, CausalJPF_State and MutationTesting. STVRDepen statically computes the program dependencies of a program, which including data dependence, control dependence, potential dependence and interactive dependence. CausalJPF_State is the implementation of dependence guided symbolic execution, which aims at improving the efficiency of symbolic execution. MutationTesting is used to conduct mutation testing, which is able to evaluate the fault detection capability of the test suite.

The project STVRDepen computes the program dependencies of a program, which is implemented based on the existing tool Indus. The Indus tool can be obtained here. The control dependence and data dependence can be simply retrieved from Indus. As for the potential dependence and interactive dependence, we compute them using the information flow analysis available in Indus.

The project CausalJPF_State conducts the dependence guided symbolic execution, which is implemented based on Symbolic PathFinder. The source code of Symbolic PathFinder can be obtained here. We extend Symbolic PathFinder with a customized listener to load the results of static program dependence analysis, and use the results to guide symbolic execution. The project CausalJPF_State consists of four sub-projects: relycalc, jpf-core, jpf-symbc and jpf-tcr. The sub-project relycalc is used to compute the program dependencies of the program, which is implemented through the jar file of the project STVRDepen. The sub-project jpf-core is the core implementation of Java Pathfinder. The sub-project jpf-symbc is the symbolic execution extension to Java PathFinder. The sub-project jpf-tcr is the extension of our approach on Symbolic PathFinder.

The sub-project MutationTesting conducts mutation testing for the given program and its mutants.

The benchmark can be downloaded here, and further details are described in the Readme file contained in the downloaded package.

Note:

Because our paper is under review, maybe we do not provide all details of our benchmarks and prototype tools. If there is any problem with the usage, please contact with hjwang@sei.xjtu.edu or tingliu@mail.xjtu.edu.cn.