Nate Yazdani
nyazdani@cs.washington.edu
@nate_yazdani
Paul G. Allen School of Computer Science & Engineering
University of Washington, Seattle
I’m a master’s student in the PLSE research group at UW CSE. I’m currently working with Dan Grossman, Talia Ringer, and John Leo on new kinds of proof automation to support the evolving nature of formal verification projects in Coq.
As an undergraduate at UW CSE, 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.
current projects
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.
recent news
| 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! |