About Me

Hello! I am a PhD Student in the Programming Systems Group @ UCSD.
I mostly work at the intersection of programming languages and security, focusing on pragmatic verification. Ultimately, I want my work to meaningfully reduce the number of bugs that exist in code.
Before joining UCSD, I worked as a Software Engineer at Dimensional Fund Advisors and completed my undergrad at Boston University where I worked on Formally Verifying Algorithms for Differential Privacy, with Professor Marco Gaboardi (BU) and Professor Arthur Azevedo De Amorim (RIT).

Projects

Verified Tock Talk - Rust Verification Workshop - Repo
Verification of process isolation in the Tock Embedded OS using Flux, a lightweight verifier for Rust.

Verified Differential Privacy for Finite Computers Extended Abstract - Talk
Verifying algorithms This extended abstract details part of my work on verifying algorithms for Differential Privacy using the Coq Proof Assistant. I submitted and presented this work at CoqPL 2023. Since then, I have verified two "fast" implementations of the Geometric Mechanism, and have worked on verifying a few other DP Mechanisms using a library derived from my original work.

Heat Adjusted Power Site
Heat Adjusted Power is the only model that is able to adjust cyclist's effort level for ambient temperature. This site was formally launched as a product by CCNS. Big thanks to Professor Michael Kane (Yale) for his guidance.

Education & Work Experience

University of California, San Diego Ph.D. Student in Computer Science, advised by Ranjit Jhala and Deian Stefan.
Boston University - Computer Science I graduated with a B.A. in CS from BU in May of 2022.
Dimensional Fund Advisors - Software Engineer I worked as a software engineer at DFA from 2022 - 2024.