Registered user since Sat 15 Aug 2020
I am a PhD Student at Cornell University in the area of Logic, Semantics, and Formal Methods, advised by Alexandra Silva. My research focuses on unified logical foundations for correctness and incorrectness reasoning. I am developing Outcome Logic, which unifies program analysis across two dimensions. First, it unifies correctness and incorrectness reasoning within a single program logic, and second, it does so across execution models (e.g., nondeterministic and probabilistic). This work has the promise to underly a new generation of static analysis tools that can be used both for verification and bug-finding.
Before coming to Cornell, I worked at Facebook as a software engineer for six years. During this time, I was fortunate to have some really great opportunities including using dependently typed Haskell in production, formally verifying concurrent algorithms for an OS microkernel, and experimenting with an information flow control type system for the Hack language. I strive to ground my research in these invaluable experiences.
Contributions