I am a Ph.D. student at the Department of Computer Science of Yale University. My advisor is Zhong Shao and I am a member of the FLINT research group. I have completed my undergraduate studies at Carnegie Mellon university. My research interests are programming languages and software verification.
I think that formally specified and certified software is an important next step in software development. There will be fewer bugs in the code, and it will enable end-users and developers to ensure that software satisfies their requirements, whatever these requirement may be. I am glad to be a part of the research effort that will make this happen.
My research effort focuses on the problem of lack of reusability in formally certified methods. It is my opinion that much of the current attempts at verification result in a one-shot approach, where the entire project is certified against a single specification, with methods that are chosen specifically for this project. Because of the ad-hoc nature of such verification attempts, it is hard to reuse the results.
My current approach to this problem is to define a framework for creation of reusable certified modules. The challenge is to enable each module to be certified independently at its own level of abstraction, and also to provide methods for linking these modules, so that certification of complex systems becomes possible.
The papers about this work are currently in progress. This research also resulted in a trace-based software verification approach, which is worked on by other members of our team.
This research has roots in an earlier work on Certified Assembly Programming, a project where I was a participant. There our group was developing methods for using foundational proof-carrying code techniques to verify assembly code as well as to reason about stack-based workflow these problems presented. My work has helped develop a logic for reasoning with exceptions and non-local jumps. I have also helped with the work on certification of self-modifying code by certifying an operating system bootloader.
Publications that relate to this work are:
- Modular Verification of Assembly Code with Stack-Based Control Abstractions
by Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. Appeared in POPL'06. - Certified Self-Modifying Code
by Hongxu Cai, Zhong Shao, and Alexander Vaynberg. Appeared in PLDI'07.
I enjoy explaining challenging concepts to people. It is very rewarding to see students gain an understanding of a complicated subject. For this reason, I have an extensive experience of being a teaching assistant for many classes:
| Semester | Class Name | Professor | University |
|---|---|---|---|
| Spring 2010 | CS 422 Operating Systems | Bryan Ford | Yale |
| Fall 2009 | CS 421 Compilers and Interpreters | Zhong Shao | Yale |
| Spring 2009 | CS 112 Intro to Programming | Daniel Abadi | Yale |
| Fall 2008 | CS 112 Intro to Programming | Drew McDermott | Yale |
| Spring 2008 | CS 422 Operating Systems | Zhong Shao | Yale |
| Fall 2007 | CS 421 Compilers and Interpreters | Zhong Shao | Yale |
| Spring 2006 | CS 422 Operating Systems | Zhong Shao | Yale |
| Fall 2005 | CS 421 Compilers and Interpreters | Zhong Shao | Yale |
| Fall 2003 | 15-212 Principles of Programming | Stephen Brookes | Carnegie Mellon |
It is unfortunate that almost all the programming that I have done recently has been for research related activities rather than for personal non-scientific interest. Due to my teaching and work, I specialize in functional programming in ML-like languages as well as low-level operating system code written in C and assembly.
My personal programming interests are usually directed towards creation of protocols / interfaces and attempts to make things more general. Here are a few examples I have toyed with, but never had the chance to bring to completion:
- A distributed peer-to-peer DNS system based on word-of-mouth trust. The same approach can be used to create a peer-to-peer Facebook clone - a definite improvement for privacy control.
- An update to the Linux input system to allow general interpretation of HID reported features. The last time I looked at the usbhid driver, it made a general guess, which was wrong for many devices. To address this issue, a specialized driver was written for many devices. I have submitted a few patches to the kernel that addressed issues in the general driver that were causing it to lose components, but I never got around to finalizing the general design. I have also written kernel patches to address issues specific to MS Strategic Commander (a left handed mouse-like joystick), but these patches are outdated, so I do not provide them.
- A REST-based protocol for media servers to replace DLNA. In my opinion DLNA is overly complex, and has too many shortcomings, such as an inability to address a server across subnets.