I'm an assistant professor in the CS Department at the Courant Institute of New York University. I'm interested in programming languages and formal verification, particularly for concurrent and randomized programs.

I received my Ph.D. from CMU, where I was advised by Robert Harper. I was then a post-doc in the PDOS group at MIT. Before coming to NYU I was an assistant professor at Boston College for a few years.

*Later credits: resourceful reasoning for the later modality*

S. Spies, L. Gäher, J. Tassarotti, R. Jung, R. Krebbers, L. Birkedal, D. Dreyer.

**ICFP 2022**[.pdf]*Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning*

T. Chajed, J. Tassarotti, M. Theng, M. F. Kaashoek, N. Zeldovich.

**OSDI 2022**[.pdf]*A Separation Logic for Negative Dependence*

J. Bao, M. Gaboardi, J. Hsu, J. Tassarotti.

**POPL 2022**[arxiv]*Rabia: Simplifying State-Machine Replication Through Randomization*

H. Pan, J. Tuglu, N. Zhou, T. Wang, Y. Shen, X. Zheng, J. Tassarotti, L. Tseng, R. Palmieri.

**SOSP 2021**[arxiv]*GoJournal: a verified, concurrent, crash-safe journaling system*

T. Chajed, J. Tassarotti, M. Theng, R. Jung, M. F. Kaashoek, N. Zeldovich.

**OSDI 2021**[.pdf]*Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic.*

S. Spies, L. Gäher, D. Gratzer, J. Tassarotti, R. Krebbers, D. Dreyer, L. Birkedal.

**PLDI 2021**[.pdf]*A formal proof of PAC learnability for decision stumps*

J. Tassarotti, K. Vajjha, A. Banerjee, J.-B. Tristan.

**CPP 2021**[arXiv]*Verifying concurrent Go code in Coq with Goose*

T. Chajed, J. Tassarotti, M. F. Kaashoek, N. Zeldovich.

**CoqPL 2020***Verifying concurrent, crash-safe systems with Perennial*

T. Chajed, J. Tassarotti, M. F. Kaashoek, N. Zeldovich.

**SOSP 2019**[.pdf]*Argosy: Verifying Layered Storage Systems with Recovery Refinement*

T. Chajed, J. Tassarotti, M. F. Kaashoek, N. Zeldovich.

**PLDI 2019**[.pdf]*Scaling Hierarchical Coreference with Homomorphic Compression*

M. Wick, S. Panda, J. Tassarotti, J.-B. Tristan

**AKBC 2019**[.pdf]*Sketching for Latent Dirichlet-Categorical Models*

J. Tassarotti, J.-B. Tristan, M. Wick.

**AISTATS 2019**[.pdf]*A Separation Logic for Concurrent Randomized Programs*

J. Tassarotti, R. Harper.

**POPL 2019**[.pdf] [Coq source]*MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic*

R. Krebbers, J.-H. Jourdan, R. Jung, J. Tassarotti, J.-O. Kaiser, A. Timany, A. Charguéraud, D. Dreyer.

**ICFP 2018**[.pdf] [website with Coq source]*Verified Tail Bounds for Randomized Programs*

J. Tassarotti, R. Harper.

**ITP 2018**[.pdf] [Coq source] [publisher's version]*Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms*

J. Tassarotti

**Draft 2017**[.pdf] [arXiv]*A Higher-Order Logic for Concurrent Termination-Preserving Refinement*

J. Tassarotti, R. Jung, R. Harper.

**ESOP 2017**[.pdf] [website with Coq source] [arXiv] [publisher's version]*Efficient Training of LDA on a GPU by Mean-for-Mode Estimation.*

J.B. Tristan, J. Tassarotti, G. L. Steele Jr.

**ICML 2015**[.pdf]*Verifying Read-Copy-Update in a Logic for Weak Memory.*

J. Tassarotti, D. Dreyer, V. Vafeiadis.

**PLDI 2015**[.pdf] [website with Coq source]*Augur: Data-Parallel Probabilistic Modeling.*

J.B. Tristan, D. Huang, J. Tassarotti, A. C. Pocock, S. J. Green, G. L. Steele Jr.

**NIPS 2014**[.pdf]*RockSalt: Better, Faster, Stronger SFI for the x86.*

G. Morrisett, G. Tan, J. Tassarotti, J.B. Tristan, and E. Gan.

**PLDI 2012**[.pdf]

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