Concise Bug Explanation via SMT Solver
In this project, we developed a tool that produces concise explanations for deep semantic bugs with the aid of an SMT solver. Specifically, given a known crashing program, the tool converts the program to SMT formula and uses an elimination algorithm based on Microsoft Z3 prover to solve for the minimal set of source code relevant to the bug. The tool significantly reduces the effort required to debug large programs that produce millions of lines of stack trace, and serves as a good complement to fuzz-testing.
Originally, we planned to use the outputs of this tool as the first stage of a deep learning system that learns to detect and explain bugs in a more efficient manner. However, the amount of crashing programs on Google’s OSS-Fuzz – an open source online fuzzing platform – did not grow as we had expected. We eventually decided not to move forward with the project.
