This summer, I worked with Professor Mayur Naik on Concise Bug Explanation Using SMT Solver. The project aims at helping programmers reason about software bugs in large scale projects, which can be extremely hard to debug due to their high complexity. A concrete use case is fuzz testing – a technique which continuously tests a program against generated inputs until it crashes. In recent years, Fuzz testing has been increasingly adopted by developers. However, even state-of-the-art fuzzers can only output the stack trace of a buggy execution, which is ambiguous and may sometimes evade the source of the bug. Our project targets this problem by producing concise “explanations” of crashing executions. Conceptually, we minimize an error trace under the constraint that the crash is retained. This way programmers can follow the minimal trace to efficiently reason about bugs in their code.
Throughout the process, I learned a lot of technical skills as well as transferable skills. On the technical side, I became relatively experience with LLVM Compiler platform and Microsoft Z3 prover, both are widely used in academia as well as industry. I also familiarized myself with concepts like Satisfiability Modulo Theories and compilation process. On the nontechnical side, I experienced the ups and downs of conducting academic research. One thing that impresses me is how we strived to formulate the problem. As my mentor said, lots of people can solve a complex problem, but few can find the right problem to solve. Despite the difficulties I encountered, participating in this research reinforces my intention to progress further in academia.
This summer, I worked with Professor Mayur Naik on Concise Bug Explanation Using SMT Solver. The project aims at helping programmers reason about software bugs in large scale projects, which can be extremely hard to debug due to their high complexity. A concrete use case is fuzz testing – a technique which continuously tests a program against generated inputs until it crashes. In recent years, Fuzz testing has been increasingly adopted by developers. However, even state-of-the-art fuzzers can only output the stack trace of a buggy execution, which is ambiguous and may sometimes evade the source of the bug. Our project targets this problem by producing concise “explanations” of crashing executions. Conceptually, we minimize an error trace under the constraint that the crash is retained. This way programmers can follow the minimal trace to efficiently reason about bugs in their code.
Throughout the process, I learned a lot of technical skills as well as transferable skills. On the technical side, I became relatively experience with LLVM Compiler platform and Microsoft Z3 prover, both are widely used in academia as well as industry. I also familiarized myself with concepts like Satisfiability Modulo Theories and compilation process. On the nontechnical side, I experienced the ups and downs of conducting academic research. One thing that impresses me is how we strived to formulate the problem. As my mentor said, lots of people can solve a complex problem, but few can find the right problem to solve. Despite the difficulties I encountered, participating in this research reinforces my intention to progress further in academia.