About Me

I am a second-year computer science Ph.D. student at Carnegie Mellon University, advised by Prof. Bryan Parno. My interests lie broadly in formal methods and programming languages.

I currently work on verifying the Rust standard library, using the verification tool Verus. Past projects include automating verification of collision avoidance, verifying implementations of distributed systems protocols, and extending CompCert guarantees to concurrent programs.

I am grateful to be supported by the NSF Graduate Research Fellowship.

News

• 10/3/25: I presented at the New England Systems Verification Day 2025!
Title: Verifying the Rust Standard Library Using Verus

• 5/6/25: I presented at the Rust Verification Workshop 2025!
Title: Initial Steps Toward Verifying the Rust Standard Library Using Verus

Background

I received a dual B.S. in computer science and mathematics and an M.S. in computer science from the University of Michigan.

At Michigan, I was part of the MARVL research group, led by Prof. Jean-Baptiste Jeannin. From 2021-2022, I worked with Nishant Kheterpal on automating and certifying proofs of collision avoidance, using the Prototype Verification System (PVS).

In 2023, I interned with Sandia National Laboratories, under the mentorship of Dr. John Bender. Our goal was to extend CompCert guarantees to concurrent programs. My part was proving that our memory model of concurrency behaved as expected, using the Rocq proof assistant.