I will be happy to work with PhD students who are interested in pursuing a research career after graduation. Broadly speaking, I work on two types of research problems:
- Verification: For example, can we formally verify that critical systems are designed correctly, their implementations have no runtime errors, and when running on real devices, they have no safety violations or security vulnerabilities?
- Program synthesis: For example, can we generate software code from some formal or informal specifications? What are the compelling applications where synthesized code offers a better solution manually-written code?
We are developing innovative solutions to these two problems, as part of a principled design of systems to improve software reliability, security, and fairness. Example topics that we explored recently include “concurrency”, “side channel”, and “AI safety/fairness”.
If you are interested in joining our group, please send your resume with the email subject “Applicant: your_name”.