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 mathematically rigorous solutions to these two problems, as part of principled design of systems to improve safety, security, and fairness. Example applications include “side channel security”, “concurrency”, “AI safety” and “fairness”.
If you are interested in joining our group, please send your resume with the email subject “Applicant: your_name”.