Hello! I am a PhD student at Northeastern University’s Khoury College of Computer Sciences, in the Programming Research Laboratory, where I conduct research in formal methods and programming languages. Right now, I am on internship with BedRock Systems, applying formal methods to real-world software infrastructure using the Coq theorem prover and the Iris logical framework.
Previously, I was a BS/MS student at the University of Washington’s Paul G. Allen School of Computer Science & Engineering, in the Programming Languages & Software Engineering research group, where I worked with Ras Bodik, Dan Grossman, John Leo, and Talia Ringer. As an undergraduate, I was honored to receive research recognition from the CRA and a Washington Research Foundation Fellowship. If you’d like to read more about my undergraduate research experience, an interview is available here.
FCSL: Fine-grained Concurrent Separation Logic
Modular verification of generic techniques in concurrent programming, in particular concurrent elimination. Working with Aleks Nanevski, leader of the broader FCSL project.
PUMPKIN PATCH: Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
Proof-engineering tooling to automate updates of proofs, definitions, and types when dependencies change. Check out the official project page here.
|Jan 8, 2018||Published early progress on proof repair in CPP 2018: paper.|
|Jun 18, 2017||Interning at IMDEA Software this summer, working with Aleks!|