BugRedux is a general framework for supporting in-house debugging of field failures. BugRedux synthesizes, using execution data collected in the field, executions that mimic the observed field failures. Our approach is based on symbolic execution and has two key aspects. First, it uses the execution data from the field to identify a set of intermediate goals that can guide the exploration of the solution space. Second, it uses a heuristic based on distance to select which states to consider first when trying to reach an intermediate goal during the exploration.

System Requirements:

BugRedux currently works on Linux, and we have not yet tried to compile it on other platforms. The tool relies on the symbolic execution engine KLEE and on the LLVM compiler infrastructure.

We have tested our latest release of BugRedux on a current version of KLEE that uses LLVM 2.9. Please contact us if you can't find KLEE's installation manual on the version that uses LLVM 2.9.


BugRedux now is a part of F3. You can find the last version here.


1. After downloading our source package, go into the "klee" directory and follow the steps listed on KLEE's "Getting Started" page (except for Step 3 in KLEE's GetStarted page, as you will be using our customized version of KLEE).

2. Make sure you build our customized KLEE with POSIX runtime support (also explained on KLEE's "Getting Started" page.)

3. Make also sure that you build KLEE with the most recent version of STP. We found some bugs in previous versions of STP that prevented our tool from working.

Example of Use of BugRedux:

1. Download and build Coreutlls 6.10 by following the instructions on the "Coreutils Case Study" page. Important: make sure to use version 6.10 of Coreutlls instead of version 6.11, as mentioned in the page--some of the faults we use to demonstrate BugRedux were removed in the newer version of CoreUtils.

2. Download the example.pl script, replace "KLEE_PATH" at the beginning of the script with your path to the "klee" executable, and read the comments in the script to get information on how the script operates. The script, when rerun, allows you to run BugRedux on one of the programs on the CoreUtils. You should be able to follow the same steps and run BugRedux on other C programs which have been built into LLVM bytecode format.


If you have any question about this tool, feel free to contact Wei Jin.

Updated: October 18, 2013