Academic

Background

I have been a student (although not a very good one) for as long as I can remember. I'm still in school right now. Someday I'll be finished with school only to return to school as a professor, but that's a while ahead.

Right now I'm at the University of Texas at Austin as a graduate student in the Department of Computer Science, working under Professor Calvin Lin.

I received my Bachelor of Arts in Computer Science at Cornell University. During my time there, I did research with the Cornell Network Research Group and later the Autonomous Underwater Vehicle Team.

Some additional details are in my resume.

Research Agenda

I am interested in lightweight static analysis for program verification. Bugs and security vulnerabilities plague commonly used software systems today. As the best cure is prevention, I am developing techniques for analyzing source code for these bugs and vulnerabilities, allowing the programmer to fix them before it becomes an issue.

Central to this is the conflict between precision and speed. If an analysis takes too long or too much memory, it is not practical for large programs. If an analysis returns many false positives, it is of very little use to a programmer, who will not want to sort through hundreds or thousands of errors looking for the real one. The tradeoff between speed and precision, and more importantly, determining the right amount of precision, is an open research area.

This raises several interesting questions:

• What types of problems are amenable to static analysis?
• What level of expressiveness is required to check a given error?
• How much precision (and what type of precision) is required to reasonably check a given error?
• What existing techniques are best suited for different problems, and what tradeoffs do they make?
• How can existing techniques be combined to improve performance and precision?
• Can the results of static analysis be used to improve the programmer's understanding of the program?

Currently, I am working on extending the Broadway compiler and analysis framework and pushing dataflow analysis for error checking to its limits. A fast dataflow analysis engine with adaptive-precision pointer analysis can deliver highly accurate results in reasonable time. While techniques like model checking can deliver even more accurate results, they suffer from serious scalability issues as the program gets larger and as aliasing relations among the variables become more common. Dataflow analysis can either be augmented to be slightly more precise with respect to handling common constructs or be used as a fast preprocessing phase for a more precise (but more time-consuming) analysis.

Publications will be available here when they get published. Stay tuned.