About Me

Hello! I am a PhD Student in the Programming Systems Group @ UCSD.
My interests currently lie in lightweight verification. I mostly work on verification tools (like Flux) and on verifying security properties of complex systems. 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

CoqPL Talk on Verified Differential Privacy You can read the extended abstract below.

Verified Differential Privacy for Finite Computers 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.

Flux - Refinement Types for Rust I actively contribute to Flux, a lightweight verification tool for Flux.

Verified Tock I actively contribute to VTock - a project aiming to verify security properties for the Tock Embedded Operating System.

A Primer on Property Based Testing for Python - Source Code PyBT is a python library for property based testing I created, in an effort to get my fellow engineers to use verification-like methods.

Heat Adjusted Power 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

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.