Industry Experience

Agentic Automated Reasoning Group, with Dr. Rustan Leino

• Designed Dafny extension ideas with first-class region and uniqueness types.
• Focused on verification performance and stronger abstraction boundaries for verified software.

Automated Reasoning in Identity, with Jenny Xiang

• Applied an immutability type checker to internal AWS code.
• Implemented Dafny-to-Java compiler support for immutability annotation translation.