Elanor Tang

About Me

I am a first-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 Rust verification, using the Verus tool. 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.

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 worked with Steven Schaefer on verifying implementations of distributed systems protocols, building on and using the Ivy verification tool.

In 2023, I did a summer internship 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 Coq proof assistant.