I am an Assistant Professor of Computer Science at the Stevens Institute of Technology in Hoboken, NJ. I develop mathematical foundations for program logics and build automated tools that bring formal verification to real-world software at scale.
I received 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.
The goal of my research is to make complex software systems trustworthy. I develop mathematical foundations for reasoning about programs and build automated tools that apply those ideas to large codebases, with the theory and the tools each informing the other. I am currently working on the following research directions:
Many programs combine computational effects in ways that existing techniques cannot yet analyze. Using Outcome Logic as a foundation, I am broadly interested in developing semantic models and logical techniques for new combinations of effects, and in finding ways to generalize them. For example, Probabilistic Concurrent Outcome Logic, which received a Distinguished Paper Award at POPL 2026, introduces new compositional reasoning techniques for randomized concurrent programs. However, significant open questions remain in supporting full concurrent reasoning for randomized programs.
AI agents can now verify software, but doing so is very computationally intensive. Theorem estimates that proving memory safety for OpenSSL would cost about $220K using LLMs. Meanwhile, Meta's Pulse-X, a symbolic analyzer, ran on OpenSSL in 16 minutes, at next to no cost. Although Pulse-X is only a bug finder, its symbolic reasoning engine is orders of magnitude more efficient than an LLM, which analyzes programs as text. I am working on tools based on Outcome Separation Logic that close the gap between the efficiency of symbolic reasoning and the expressive power of AI.
AI-generated software artifacts are quickly becoming too large for engineers to understand. Verification can help, but is only useful if the specifications are auditable, meaning that a human can read them and clearly understand what was actually proved. Auditability is especially difficult in massive build artifacts, where interactions between different programming languages and effects make specifications more complicated. I am interested in interoperable logics and formal libraries that keep specifications understandable across these boundaries.
@article{zilberstein2026denotational,
title = {{Denotational Semantics for Probabilistic and Concurrent Programs}},
author = {Zilberstein, Noam and Gorla, Daniele and Silva, Alexandra},
journal = {ACM Trans. Program. Lang. Syst.},
year = 2026,
month = oct,
publisher = {Association for Computing Machinery},
doi = {10.1145/3840298},
url = {https://doi.org/10.1145/3840298}
}
@phdthesis{zilberstein2026semantic,
title = {{Semantic and Logical Foundations for Randomized Concurrent Programs}},
author = {Zilberstein, Noam},
school = {Cornell University},
year = 2026,
month = aug,
url = {https://www.proquest.com/dissertations-theses/semantic-logical-foundations-randomized/docview/3385352698/se-2}
}
@article{zilberstein2026probabilistic,
title = {{Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants}},
author = {Zilberstein, Noam and Silva, Alexandra and Tassarotti, Joseph},
journal = {Proc. ACM Program. Lang.},
volume = 10,
number = {POPL},
articleno = 9,
numpages = 30,
year = 2026,
month = jan,
publisher = {Association for Computing Machinery},
doi = {10.1145/3776651},
url = {https://doi.org/10.1145/3776651}
}
@article{zilberstein2025outcome,
title = {{Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects}},
author = {Zilberstein, Noam},
journal = {ACM Trans. Program. Lang. Syst.},
volume = 47,
number = {3},
numpages = 71,
year = 2025,
month = sep,
publisher = {Association for Computing Machinery},
doi = {10.1145/3743131},
url = {https://doi.org/10.1145/3743131}
}
@inproceedings{zilberstein2025denotational,
title = {{Denotational Semantics for Probabilistic and Concurrent Programs}},
author = {Zilberstein, Noam and Gorla, Daniele and Silva, Alexandra},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
editor = {Bouyer, Patricia and van de Pol, Jaco},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = 348,
pages = {39:1--39:24},
year = 2025,
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
doi = {10.4230/LIPIcs.CONCUR.2025.39},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2025.39}
}
@article{zilberstein2025demonic,
title = {{A Demonic Outcome Logic for Randomized Nondeterminism}},
author = {Zilberstein, Noam and Kozen, Dexter and Silva, Alexandra and Tassarotti, Joseph},
journal = {Proc. ACM Program. Lang.},
volume = 9,
number = {POPL},
articleno = 19,
numpages = 30,
year = 2025,
month = jan,
publisher = {Association for Computing Machinery},
doi = {10.1145/3704855},
url = {https://doi.org/10.1145/3704855}
}
@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},
journal = {Proc. ACM Program. Lang.},
volume = 8,
number = {OOPSLA2},
articleno = 300,
numpages = 30,
year = 2024,
month = oct,
publisher = {Association for Computing Machinery},
doi = {10.1145/3689740},
url = {https://doi.org/10.1145/3689740}
}
@article{zilberstein2024outcome,
title = {{Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects}},
author = {Zilberstein, Noam and Saliling, Angelina and Silva, Alexandra},
journal = {Proc. ACM Program. Lang.},
volume = 8,
number = {OOPSLA1},
articleno = 104,
numpages = 29,
year = 2024,
month = apr,
publisher = {Association for Computing Machinery},
doi = {10.1145/3649821},
url = {https://doi.org/10.1145/3649821}
}
@article{zilberstein2023outcome,
title = {{Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning}},
author = {Zilberstein, Noam and Dreyer, Derek and Silva, Alexandra},
journal = {Proc. ACM Program. Lang.},
volume = 7,
number = {OOPSLA1},
articleno = 93,
numpages = 29,
year = 2023,
month = apr,
publisher = {Association for Computing Machinery},
doi = {10.1145/3586045},
url = {https://doi.org/10.1145/3586045}
}
@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},
booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
series = {CPP 2022},
pages = {116--129},
year = 2022,
month = jan,
publisher = {Association for Computing Machinery},
doi = {10.1145/3497775.3503681},
url = {https://doi.org/10.1145/3497775.3503681}
}
@inproceedings{zilberstein2020eliminating,
title = {{Eliminating Bugs with Dependent Haskell (Experience Report)}},
author = {Zilberstein, Noam},
booktitle = {Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell},
series = {Haskell 2020},
pages = {9--16},
year = 2020,
month = aug,
publisher = {Association for Computing Machinery},
doi = {10.1145/3406088.3409020},
url = {https://doi.org/10.1145/3406088.3409020}
}