In recent years, several logical foundations have been proposed for bug-finding analyses. The key feature of those logics is the ability to identify true positive bugs. Infer, a static analyzer developed at Meta, is based on Incorrectness Logic. But the implementation of Infer differs from the theory when it comes to the handling of functions for which no specification is available, leading to false positives. In this talk, I present a new strategy for modeling incorrectness in the presence of unknown functions using a combination of angelic and demonic nondeterminism.

I am a final year PhD Candidate at Cornell University in the area of Programming Languages and Formal Methods, advised by Alexandra Silva. Before coming to Cornell, I was a staff software engineer in the Facebook Programming Languages and Runtimes team, where I was fortunate to work on unique projects including using dependently typed Haskell in production and formally verifying concurrent algorithms for an OS microkernel.

My research focuses on logical foundations for reasoning about programs that branch into different outcomes, which provide a unifying perspective for reasoning about a wide variety of effects including nondeterminism, nontermination, randomization, concurrency, and exceptions. Through my research, I have developed Outcome Logic, which has applications including unifying the theories of correctness and incorrectness and verification of concurrent randomized algorithms.

I am on the market for tenure track academic positions. See my research statement and CV for more information.