Research

I study the Rust programming language, which can guarantee memory and thread safety without run-time overhead. Rust’s borrow checker provides these guarantees by restricting the programs that developers can write. When these restrictions become burdensome, developers can enable a set of unsafe features that bypass the borrow checker. However, these features are difficult to use correctly, as they can lead to security vulnerabilities.

My goal is to make it easier for developers to use unsafe correctly. To make this possible, I am currently researching methods for gradually verifying that Rust programs are free of undefined behavior. Gradual verification enables developers to write partial, incomplete specifications for their programs, with the remaining properties checked at run-time. A gradual version of Miri’s Tree Borrows model will enable Rust developers to lift their test cases step-by-step into complete, static specifications that their programs are free of undefined behavior.

Recent Publications

Education

I attended the University of Wisconsin-Eau Claire from 2017 to 2021. I completed a double major in Computer Science and English with a minor in Mathematics. I was introduced to Computer Science research by Chris Johnson, and I helped contribute to the design of Twoville: a direct manipulation programming system for computer science education.

In 2020, I was accepted into CMU’s REUSE program, where I joined a collaboration between CMU and Arizona State University. We created TTPython, a macroprogramming systems for the Internet of Things. We used our prototype to implement a mock autonomous vehicle intersection and observed significantly reduced latency compared to a prior approach.

I began my PhD in Software Engineering at CMU in September, 2021. My current research on Rust is funded by the National Science Foundation’s Graduate Research Fellowship Program (GRFP). I’m advised by Jonathan Aldrich and Joshua Sunshine in S3D.