About Me
I currently work at MatX, where I perform formal verification on hardware. Before that, I worked on hardware formal verification at Rivos and then Meta after Meta acquired Rivos.
In June 2025, I successfully defended my PhD dissertation, Theorem-Prover-Assisted Counterexample Generation with Constrained Enumerative Types at Northeastern University's Khoury College. My PhD advisor was Panagiotis "Pete" Manolios. I regularly collaborated with Ankit Kumar, another student of Pete's.
My research area is formal methods. In particular, I am interested in combining theorem provers, constraint solvers, and enumerative data types (along the lines of CGEN) to better generate data satisfying certain constraints. I've used this approach to fuzz parts of complex protocols (like the 802.11 WiFi specification).
I am the current maintainer of the ACL2s Eclipse plugin.
I was a Front Desk Volunteer at the Artisans Asylum makerspace in Allston, MA. from 2019-2025.
