Union-Find and Usability: A Verification Case Study
Are automated Rust verifiers usable by programmers without a formal methods background?
At LLNL,
I conducted a case study using the Prusti
and Creusot formal verification tools.
Both tools were used to verify the correctness of a union-find implementation within the E-graphs project, egg.
I found that while Prusti was more user-friendly in terms of UI, Creusot made it easier to verify more complex properties.
Situationally Adaptive Language Tutor (SALT)
Building on the work of REVIS
and the error analysis study I conducted over summer 2023, I designed a custom logging system for programmer actions in VS Code
to gather minimally invasive data on IDE interactions and compiler errors made by Rust programmers participating in our study. My lab is currently working on discovering which
programming decisions (and mistakes) correlate to learning progression in the Rust programming language!
Rust Compiler Error Analysis
What are the most frequent and costly errors for programmers to fix, and how can we design tools to make debugging them more efficient?
I analyzed 10,957 Rust diagnostic messages recorded from students and categorized them into 1916 distinct resolution sessions to analyze error frequency and average time taken to resolve.
As a result, I found that ownership errors, while less frequent, took longer on average to fix.
Privacy Perspectives in VR
To understand how VR users and gamers view personal privacy, I surveyed 40 participants to find out which circumstances meet or do not meet their privacy expectations.
I found that greatest concern lies in how biometric data and third party data is handled, and those who use VR platforms more frequently have significantly lower privacy expectations than those who do only occasionally.
In our WIPS paper, we focused on children's privacy in gaming and VR.