Noam Zilberstein

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.

News

Dec ’22

My paper on Outcome Logic with Derek Dreyer and Alexandra Silva was conditionally accepted to OOPSLA 2023

Dec ’21

I was selected to participate in this year’s POPL Student Research Competition

Nov ’21

My paper on formal verification work that I did at Facebook has been accepted to CPP

Nov ’21

I will be speaking at the Facebook Testing and Verification Symposium next month

Sep ’21

After 6 years, I am leaving Facebook to start my PhD at Cornell University

Preprints

Dec   ’22

Publications

CPP  ’22
Quentin Carbonneaux, Noam Zilberstein, Peter O'Hearn, Christoph Klee, Francesco Zappa Nardelli