Research Interests
At Microsoft, I am one of the contributors to project SAGE, which is the abbreviation of "Scalable Automated Guided Execution". SAGE is a while-box fuzzing tool that can analyze the execution instructions of a program and use constraint solving techniques to search the inputs that can break the program, such as crash, hang or other abnormal behaviors. SAGE is an amazing tool. It won two gold medals out of three in Fuzzing Olympic 2008 (Microsoft Internal), with the titles as the most effective and the best overall fuzzer. You can get more details about SAGE from this paper. SAGE is a good example that how the intelligent search power of constraint solver can help to leverage the the testing and verification technologies, of course combined with cutting-edge dynamic analysis technologies from CSE. I am glad to get an opportunity to work for such a project where my expertises can find a place :)
Now I am mainly working on Windows Azure. I cannot say too much details since Windows Azure is not fully commercialized yet. This is an exciting project and the way to work on a huge size highly distributed system is very refreshing, of course very challenging.
My past research experiences include formal and semiformal verification, testing and computer security. My Ph.D. dissertation is "Exploring Constraint Satisfiability Techniques in Formal Verification" which can be accessed here. It has been a long way to build bug free design. No matter it's hardware or software, building the "correct" design is not that easy especially when system grows bigger and more complex. Contrary to the traditional methods where designs are simulated under various expected scenarios after deployment, formal methods come up a new perspective that tries to prove the correctness without worrying about corner cases. During my PhD I am involved in various research areas, including VLSI design testing, Nano design testing and satisfiablity (SAT) solving and its applications. I proposed methods to boost SAT solver performance and improve optimized SAT solving, such as MIN-ONE SAT and MAX-SAT problems. These advanced solver algorithms can bring significant benefits to many application domains. I bought some of the SAT techniques and applied them in the power minimization and test volumn reduction in VLSI testing. These research work has demonstrated promising improvement.
My Master research can be concluded as proposing a Maximum Likelihood Estimation (MLE) based algorithm to locate wireless sensor nodes and identify any malicious nodes that attempt to provide spurious locationing information by intrusion detection techniques. Fortunately I was able to get some exciting results and published a few papers in Professor Du's research group. These papers were cited more than 80 times and one of them was awarded as best paper in algorithm track at International Parallel and Distributed Processing Symposium (IPDPS) 2005.