Joseph Tassarotti home papers teaching

Email: jt4767@nyu.edu
CV (January 2026)

I'm an associate professor in the CS Department at New York University. I'm also an Amazon Scholar at Amazon Web Services, where I work on the Dogwood policy language. I'm interested in programming languages and formal verification, particularly for concurrent and randomized programs.

News

10/2026 - Former postdoc advisee Alexandre Moine has started a position as a researcher at Inria Lyon. Congratulations, Alexandre!
09/2026 - I have been promoted to associate professor with tenure at NYU. Many thanks to my students, collaborators, mentors, and colleagues for their support along the way!
02/2026 - I am honored to have been selected as a 2026 Sloan Research Fellow. I'm grateful to my students, collaborators, and mentors who made this possible. I also appreciate the support from my department and the letter writers for my nomination. Thank you all!

PhD Students

Postdocs

Jinkun Geng

Papers

- Verifying a High-Performance Distributed Transaction System using Permissioned State Machines
- Yun-Sheng Chang, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- SOSP 2026 [pdf]
- A Separation Logic for Parallel Time Complexity with Work and Span Credits
- Alexandre Moine, Sam Westrick, Joseph Tassarotti
- ICFP 2026 [pdf]
- Completeness of Iris-Based Program Logics
- Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, Joseph Tassarotti
- ICFP 2026 [pdf]
- Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
- Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti
- LICS 2026
- Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
- Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal
- PLDI 2026 [arXiv]
- Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
- Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
- PLDI 2026 [arXiv]
- All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
- Alexandre Moine, Sam Westrick, Joseph Tassarotti
- Distinguished Paper Award
- POPL 2026 [arXiv]
- Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
- Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
- Distinguished Paper Award
- POPL 2026 [arXiv]
- Logical Relations for Formally Verified Authenticated Data Structures
- Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
- CCS 2025 [pdf]
- Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
- Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
- ICFP 2025 [arXiv]
- ParserHawk: Hardware-aware parser generator using program synthesis
- Xiangyu Gao, Jiaqi Gao, Karan Kumar G., Muhammad Haseeb, Ennan Zhai, Bili Dong, Joseph Tassarotti, Srinivas Narayana, Anirudh Sivaraman
- SIGCOMM 2025 [pdf]
- Verified Foundations for Differential Privacy
- Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan
- PLDI 2025 [pdf]
- Approximate Relational Reasoning for Higher-Order Probabilistic Programs
- Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
- POPL 2025 [arXiv]
- A Demonic Outcome Logic for Randomized Nondeterminism
- Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti
- POPL 2025 [arXiv]
- Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation
- Anish Athalye, Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, Nickolai Zeldovich
- SOSP 2024 [pdf]
- Tachis: Higher-Order Separation Logic with Credits for Expected Costs
- Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
- OOPSLA 2024 [arXiv]
- Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
- Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
- Distinguished Paper Award
- ICFP 2024 [pdf]
- Almost-Sure Termination by Guarded Refinement
- Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
- ICFP 2024 [pdf]
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
- POPL 2024 [pdf]
- Grove: a Separation-Logic Library for Verifying Distributed Systems
- Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- SOSP 2023 [pdf]
- Verifying vMVCC, a high-performance transaction library using multi-version concurrency control
- Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- OSDI 2023 [pdf]
- Verified Density Compilation for a Probabilistic Programming Language
- Joseph Tassarotti, Jean-Baptiste Tristan
- PLDI 2023 [pdf]
- Later credits: resourceful reasoning for the later modality
- Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
- ICFP 2022 [pdf]
- Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning
- Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, Nickolai Zeldovich
- OSDI 2022 [pdf]
- A Separation Logic for Negative Dependence
- Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti
- POPL 2022 [arXiv]
- Rabia: Simplifying State-Machine Replication Through Randomization
- Haochen Pan, Jesse Tuglu, Neo Zhou, Tianshu Wang, Yicheng Shen, Xiong Zheng, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
- SOSP 2021 [arXiv]
- GoJournal: a Verified, Concurrent, Crash-safe Journaling System
- Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
- OSDI 2021 [pdf]
- Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
- Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
- PLDI 2021 [pdf]
- A Formal Proof of PAC Learnability for Decision Stumps
- Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan
- CPP 2021 [arXiv]
- Verifying Concurrent Go Code in Coq with Goose
- Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- CoqPL 2020 [pdf]
- Verifying Concurrent Crash-Safe Systems with Perennial
- Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- SOSP 2019 [pdf]
- Argosy: Verifying Layered Storage Systems with Recovery Refinement
- Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
- PLDI 2019 [pdf]
- Scaling Hierarchical Coreference with Homomorphic Compression
- Michael L. Wick, Swetasudha Panda, Joseph Tassarotti, Jean-Baptiste Tristan
- AKBC 2019 [pdf]
- Sketching for Latent Dirichlet-Categorical Models
- Joseph Tassarotti, Jean-Baptiste Tristan, Michael Wick
- AISTATS 2019 [pdf]
- A Separation Logic for Concurrent Randomized Programs
- Joseph Tassarotti, Robert Harper
- POPL 2019 [pdf] [code]
- MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
- Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
- ICFP 2018 [pdf] [project site]
- Verified Tail Bounds for Randomized Programs
- Joseph Tassarotti, Robert Harper
- ITP 2018 [pdf] [source code]
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- Joseph Tassarotti, Ralf Jung, Robert Harper
- ESOP 2017 [pdf] [project site]
- Efficient Training of LDA on a GPU by Mean-for-Mode Estimation
- Jean-Baptiste Tristan, Joseph Tassarotti, Guy L. Steele Jr.
- ICML 2015 [pdf]
- Verifying Read-Copy-Update in a Logic for Weak Memory
- Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
- PLDI 2015 [pdf] [project site]
- Augur: Data-Parallel Probabilistic Modeling
- Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.
- NeurIPS 2014 [pdf]
- RockSalt: better, faster, stronger SFI for the x86
- Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan
- PLDI 2012 [pdf]

Teaching

At NYU:

Fall 2026 — Programming Languages
Fall 2025 — Programming Languages
Spring 2025 — Compiler Construction
Fall 2024 — Programming Languages
Spring 2024 — Compiler Construction
Fall 2023 — Special Topics: Verification
Spring 2023 — Compiler Construction

At Boston College:

Spring 2021, Spring 2022 — Principles of Programming Languages
Fall 2020, Fall 2021 — Formal Verification
Spring 2020 — Randomness and Computation
Fall 2019 — Randomness and Computation

Support

My work is currently supported by NSF awards 2524669, 2504143, 2338317, and 2319168, and by a Sloan Research Fellowship.