Noam Zilberstein

PhD Candidate

/

Bio

I am a PhD Candiate 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, 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 experiences. My research is supported in part by an Amazon Research Award, ARIA’s Safeguarded AI Programme, and I was recently recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software research.

Research

My research focuses on logical foundations for reasoning about randomized concurrent programs. For decades, randomization has been used to improve the performance and capabilities of distributed systems. For example, Dijkstra famously showed that the Dining Philosophers–a distributed synchronization problem–has no fully distributed deterministic solution, but it has a simple randomized one. Establishing correctness for these types of programs is notoriously difficult because of the complex ways in which random sampling interacts with concurrent scheduling. Despite this, prior to my research, there were no full semantic models for probabilistic concurrent programs, let alone mechanized formal methods to reason about them.

My work builds on Outcome Logic, a logical framework that I previously developed for reasoning about programs that branch into many different traces due to nondeterminism, probabilistic choice, or other related computational effects. One goal of this work was to unify formal methods for correctness and incorrectness, whose metatheory had diverged into the semantically incompatible Hoare Logic and Incorrectness Logic.

Publications

CONCUR  ’25 (Preprint)
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
arXiv Show BibTeX 
@inproceedings{zilberstein2025denotational, title = {Denotational Semantics for Probabilistic and Concurrent Programs}, author = {Noam Zilberstein and Daniele Gorla and Alexandra Silva}, year = 2025, booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{"u}r Informatik}, address = {Dagstuhl, Germany}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = 348, pages = {4:1--4:24}, doi = {10.4230/LIPIcs.CONCUR.2025.4}, note = {To Appear}, editor = {Patricia Bouyer and Jaco van de Pol} }
TOPLAS  ’25 (Preprint)
Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
Noam Zilberstein
DOI Show BibTeX 
@article{zilberstein2025outcome, title = {Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects}, author = {Zilberstein, Noam}, year = 2025, month = {Jun}, journal = {ACM Trans. Program. Lang. Syst.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, doi = {10.1145/3743131}, issn = {0164-0925}, url = {https://doi.org/10.1145/3743131}, note = {Just Accepted} }
POPL  ’25
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Joseph Tassarotti, Alexandra Silva, Dexter Kozen
DOI Talk Show BibTeX 
@article{zilberstein2025demonic, title = {A Demonic Outcome Logic for Randomized Nondeterminism}, author = {Zilberstein, Noam and Kozen, Dexter and Silva, Alexandra and Tassarotti, Joseph}, year = 2025, month = {Jan}, journal = {Proc. ACM Program. Lang.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 9, number = {POPL}, doi = {10.1145/3704855}, url = {https://doi.org/10.1145/3704855}, issue_date = {Jan 2025}, articleno = 19, numpages = 30 }
OOPSLA  ’24
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Linpeng Zhang, Noam Zilberstein, Benjamin Kaminski, Alexandra Silva
DOI Show BibTeX 
@article{zhang2024quantitative, title = {Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers}, author = {Zhang, Linpeng and Zilberstein, Noam and Kaminski, Benjamin Lucien and Silva, Alexandra}, year = 2024, month = {oct}, journal = {Proc. ACM Program. Lang.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 8, number = {OOPSLA2}, doi = {10.1145/3689740}, url = {https://doi.org/10.1145/3689740}, issue_date = {October 2024}, articleno = 300, numpages = 30, }
OOPSLA  ’24
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Noam Zilberstein, Angelina Saliling, Alexandra Silva
DOI Talk Show BibTeX 
@article{zilberstein2024outcome, title = {Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects}, author = {Zilberstein, Noam and Saliling, Angelina and Silva, Alexandra}, year = 2024, month = {apr}, journal = {Proc. ACM Program. Lang.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 8, number = {OOPSLA1}, doi = {10.1145/3649821}, url = {https://doi.org/10.1145/3649821}, issue_date = {April 2024}, articleno = 104, numpages = 29, }
OOPSLA  ’23
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Noam Zilberstein, Derek Dreyer, Alexandra Silva
DOI Talk Show BibTeX 
@article{outcome, title = {Outcome Logic: A Unifying Foundation of Correctness and Incorrectness Reasoning}, author = {Zilberstein, Noam and Dreyer, Derek and Silva, Alexandra}, year = 2023, month = {Apr}, journal = {Proc. ACM Program. Lang.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 7, number = {OOPSLA1}, doi = {10.1145/3586045}, url = {https://doi.org/10.1145/3586045}, issue_date = {April 2023}, articleno = 93, numpages = 29 }
CPP  ’22
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Peter O'Hearn, Christoph Klee, Francesco Zappa Nardelli
DOI Talk Show BibTeX 
@inproceedings{carbonneaux2022applying, title = {Applying Formal Verification to Microkernel IPC at Meta}, author = {Carbonneaux, Quentin and Zilberstein, Noam and Klee, Christoph and O'Hearn, Peter W. and Zappa Nardelli, Francesco}, year = 2022, booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs}, location = {Philadelphia, PA, USA}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, series = {CPP 2022}, pages = {116–129} doi = {10.1145/3497775.3503681}, isbn = 9781450391825, url = {https://doi.org/10.1145/3497775.3503681}, numpages = 14, }
Haskell  ’20
Eliminating Bugs with Dependent Haskell
Noam Zilberstein
DOI Code Talk Show BibTeX 
@inproceedings{zilberstein2020eliminating, title = {Eliminating Bugs with Dependent Haskell (Experience Report)}, author = {Zilberstein, Noam}, year = 2020, booktitle = {Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell}, location = {Virtual Event, USA}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, series = {Haskell 2020}, pages = {9}, doi = {10.1145/3406088.3409020}, isbn = 9781450380508, url = {https://doi.org/10.1145/3406088.3409020}, numpages = 8 }

Drafts

May   ’25
Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics
James Li, Noam Zilberstein, Alexandra Silva
arXiv Show BibTeX 
@misc{li2024totaloutcomelogicproving, title={Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics}, author={James Li and Noam Zilberstein and Alexandra Silva}, year={2025}, eprint={2411.00197}, archivePrefix={arXiv}, primaryClass={cs.LO}, url={https://arxiv.org/abs/2411.00197}, }
Nov   ’24
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
arXiv Show BibTeX 
@misc{zilberstein2024probabilisticconcurrentreasoningoutcome, title={Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants}, author={Noam Zilberstein and Alexandra Silva and Joseph Tassarotti}, year={2024}, eprint={2411.11662}, archivePrefix={arXiv}, primaryClass={cs.LO}, url={https://arxiv.org/abs/2411.11662}, }
Copied!