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.

Note: the following paragraph is the abstract of the research paper published on the 2017 Pioneer Research Journal. For more information, please refer to the paper.

In October 2017, Sony launched the Xperia Touch, a futuristic product that is both a projector and an Android tablet – it uses an infrared sensor to convert any flat surface to a touch screen. However, it comes with a hefty $1700 price tag. What if I tell you that most of its functionalities can be achieved with a $50 Kinect Sensor and some computer vision techniques?

These are some inspiring quotes I encountered during reading. Each of them set in motion a ripple of thoughts and deeply influenced me. Those enclosed in quotation marks are direct quotes, and the rest are paraphrases.