I welcome PhD students who are good at math and programming, and want to pursue a research career after graduation.
Broadly speaking, I work on two types of research problems:
- Verification: Can we verify that critical systems are designed correctly, their implementations do not have run-time errors, and when running on real devices, they do not have safety violations or security vulnerabilities?
- Program synthesis: Can we generate code automatically from formal or informal specifications? What are the compelling applications where synthesis offers better solutions than manually written code?
We are developing solutions to these problems, with applications to principled design of critical systems. Examples include “concurrency”, “side channel”, and “safety enforcement” in machine learning and cyber physical systems.
If you are interested in joining us, please send your resume with the subject “Applicant: your_name “.