Symbolic execution is a technique for finding software defects automatically. It is effective in generating traceable defect reports. In this project we build upon our experience with TRACER symbolic execution tool to advance further by combining the technologies we have developed with advanced symbolic execution approaches.

• NOW AVAILABLE: Ubuntu 16.04 VirtualBox VM image with Tracer-X pre-built.
  Username: ubuntu1604 & Password: 123456
• The Tracer-X early prototype is based on KLEE. It is still being actively developed by the team and not yet ready for release. In general, to build it with all the features of Tracer-X, you need to specify the --with-z3=... option to the configure script to specify the residence of Z3. To run Tracer-X, provide -solver-backend=z3 to klee. Tracer-X adds several other options to KLEE, in particular, -output-tree to output the traversed tree in the SVG format and -no-interpolation to disable interpolation. There are several example programs that we use for testing it. Needless to say, we do not have resources to provide technical support, however, please feel free to submit issues via GitHub.

• TRACER Homepage
• Source on github