ConCrash is our tool for reproducing thread-safety violations of Java classes from crash stacks. ConCrash takes in input a crash stack trace and outputs a runnable test code and one of its thread interleavings that reproduce the crash stack in input. A test code is composed of a set of method call sequences that access concurrently (on multiple threads) the public interface of the program under test.

Related publications

  • Bianchi, Pezzè, Terragni, "Reproducing Concurrency Failures From Crash Stacks", FSE 2017.
For more information and for the evaluation artifacts please contact: Francesco Bianchi


  2. Getting started
  3. Tutorial
    1. Working with the VM image
    2. Working with the binaries
    3. Replicate the experiments for FSE '17
    4. Integrate new subjects


To start using ConCrash, you can download:
  • Our VM image with ConCrash ready to useVDI
  • ConCrash binaries with dependencies GZ
  • (Binaries works with a 64-bit Linux environment)


Working with the VM image

  1. Download the VM image VDI
  2. To access the VM, use username: concrash password: concrash
  3. No additional steps are required, ConCrash is ready to be used (see Replicate the experiments for FSE '17 and Integrate new subjects)

Working with the binaries

  1. Download ConCrash binaries with dependencies GZ
  2. Install Z3: the ConCrash distribution contains the z3 executable file for Mac OSX. If you use ConCrash in a different environemnt, please install the compatible version. You need to place the executable file in the ConCrash/solvers directory and the file must be named z3
  3. Configure JPF: create a file named in ~/.jpf folder (create it if it does not exist). The file must have the following content (you need to change the first path in order to point out your ConCrash/cortex/CortexSE folder:
  4. #JPF site configuration
    jpf.home = /your/path/to/concrash/ConCrash/cortex/CortexSE/
    jpf-core = ${jpf.home}/jpf-core
    jpf-concurrent = ${jpf.home}/jpf-concurrent
    jpf-symbc = ${jpf.home}/jpf-symbc
    jpf-symbiosis = ${jpf.home}/jpf-symbiosis

Replicate the experiments for FSE'17

  1. Launch ConCrash/scripts/experiments/ to run ConCrash on the 10 subjects used in the evaluation
  2. Launch ConCrash/scripts/experiments/ to run ConCrash with the single pruning strategies enabled on the 10 subjects used in the evaluation
  3. Open the file ConCrash/output/summary_results.csv to see the results. The csv file has the following structure:
    1. TimeStamp, System time in the moment of ConCrash start
    2. Configuration, name of the file containing the transformation rules
      1. ConCrash, Original version of ConCrash with all pruning strategy enabled
      2. PS-Stack, Only PS-Stack pruning strategy enabled
      3. PS-Redundant, Only PS-Redundant pruning strategy enabled
      4. PS-Interleave, Only PS-Interleave pruning strategy enabled
      5. PS-Interfere, Only PS-Interfere pruning strategy enabled
      6. None, None pruning strategy enabled
    3. TimeBudget, Time budget in seconds
    4. RandomSeed, Random seed used in input
    5. Subject, Subject name
    6. TestName, Name of the generated test that reproduces the crash stack 
    7. FR, Whether the failure has been successfully reproduced within the time budget
    8. FRT, The overall elapsed time in seconds for identifying the first test code and failure inducing interleaving
    9. FTID, The ID of the first failure-inducing test code
    10. FTS, The size of the failure-inducing test code measured as the total number of outermost method calls in the test code

Integrate new subjects

To run ConCrash on a new subject, you need to perform the following steps:
  1. Create a directory containing your subject in ConCrash/benchmarks (e.g. ConCrash/benchmarks/MySubject)
  2. Make sure that the directory contains the following sub-directories and files
    1. src, Directory containing the source files of the subject
    2. lib, Directory containing the dependency libraries of the subject
    3. crash-stack, File reporting the crash-stack trace of the failure you want to reproduce
  3. Launch ConCrash/scripts/experiments/ to run ConCrash on the subject. The scripts takes as input the following parameters:
    1. Subject, The name of the folder you created in the benchmark folder (e.g. MySubject)
    2. TimeBudget, A time budget in seconds
    3. Configuration, The configuration you want to use (ConCrash, PS-Stack, PS-Redundant, PS-Interleave, PS-Interfere, None). This parameter is optional: if you do not specify it, the configuration ConCrash will be used.
    4. RandomSeed, A random seed to make the execution semi-deterministic
  4. Open the file ConCrash/output/summary_results.csv to see the results. See Replicate the experiments for FSE '17 for the structure of the output file