Noam Zilberstein

I am a PhD Student at Cornell University in the area of Logic, Semantics, and Formal Methods advised by Alexandra Silva. My current research focuses on program logics that generalize over computational effects (such as nondeterminism and probabilistic choice) in order to verify correctness (and incorrectness) of many different types of programs in a unified way.

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.


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


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