I am a PhD Candiate at Cornell University in the area of Logic, Semantics, and Formal Methods, advised by Alexandra Silva. My research focuses on Outcome Logic, a reformulation of Hoare Logic with computational effects at its core. Outcome Logic consolidates the metatheory behind many variants of Hoare Logic, enabling extensible reasoning about different types of programs and tying together ideas developed over that last sixty years including the seminal work of Floyd and Hoare on program logics in the 1960s, extensions of Hoare Logic to nondeterministic and probabilistic programs, monadic effects, and the more recent emphasis on formal methods for incorrectness. On the applied side, Outcome Logic reduces the engineering cost of building static analyzers, since a single engine can underly analyses for both verification and bug-finding tools across programs with varying effects. This work is supported in part by an Amazon Research Award.
Before coming to Cornell, I worked as a software engineer for six years at Facebook. During that time, I was fortunate to have unique 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.
Our paper on Outcome Separation Logic was accepted to appear at OOPSLA 2024
I’m organizing a POPL workshop on Formal Methods for Incorrectness with Azalea Raad. If you work on incorrectness, please consider submitting a talk!
This June I will be visiting the Programming Principles, Logic, and Verification Group at UCL
I will be attending the Iris Workshop at MPI-SWS to talk about my work on Outcome Separation Logic
My paper on Outcome Logic with Derek Dreyer and Alexandra Silva was conditionally accepted to OOPSLA 2023