About Me

I am an Assistant Professor of Computer Science at the Stevens Institute of Technology in Hoboken, NJ. My research centers around the semantic foundations of program logics and applications of formal methods to improve real world software quality.

I recieved my PhD from Cornell University in 2026 where I was advised by Alexandra Silva. Before Cornell, I was a staff software engineer in the Facebook Programming Languages and Runtimes team, where I applied formal methods by using dependently typed Haskell in production and formally verifying concurrent algorithms for an OS microkernel. My research has been recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software research and a distinguished paper award at POPL 2026.

I am recruiting PhD students for the 2027-28 academic year. If you are interested in working with me, please reach out and apply to Stevens!

Research

The overarching goal of my research is to develop mathematical foundations for trustworthy software systems. I combine formal reasoning, automated analysis, and AI to make complex programs more reliable. My work spans semantic foundations, scalable program analysis techniques, and infrastructure for AI-assisted verification. I am currently working on the following research directions:

  • Mathematical Foundations of Program Logics: Foundations for reasoning about complex programs, including challenging combinations of effects such as concurrency, probability, and nondeterminism.
  • Next-Generation Static Analysis: Scalable analysis techniques enhanced by generative AI to solve targeted reasoning problems while preserving the efficiency of traditional methods.
  • Infrastructure for AI-Based Program Verification: Trusted formal libraries and verification frameworks that enable AI systems to reason about programs with mathematical rigor.

Publications

POPL  ’26
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Distinguished Paper Award
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
DOI Talk Show BibTeX 
@article{zilberstein2026probabilistic, title = {{Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants}}, author = {Noam Zilberstein and Alexandra Silva and Joseph Tassarotti}, year = 2026, month = {Jan}, journal = {Proc. ACM Program. Lang.}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = 10, number = {POPL}, doi = {10.1145/3776651}, url = {https://doi.org/10.1145/3776651}, issue_date = {Jan 2026}, numpages = 30 }
TOPLAS  ’25
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} }
CONCUR  ’25
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
DOI Show BibTeX 
@inproceedings{zilberstein2025denotational, title = {{Denotational Semantics for Probabilistic and Concurrent Programs}}, author = {Zilberstein, Noam and Gorla, Daniele and Silva, Alexandra}, 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 = {39:1--39:24}, doi = {10.4230/LIPIcs.CONCUR.2025.39}, isbn = {978-3-95977-389-8}, issn = {1868-8969}, url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.39}, editor = {Bouyer, Patricia and van de Pol, Jaco}, }
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 }
Copied!