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.

Project Poster

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.

© 2021 Chuning Zhu. All rights reserved.

Powered by Jekyll and Hydejack. Hosted on Eniac.