Email: jt4767@cs.nyu.edu
CV (November 2021)

Note: As of July 1st, 2022 I have moved to New York University. This website at Boston College is out of date. You should be re-directed to my new site shortly

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.

Papers

• 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]


• 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]

Teaching

At Boston College:

• Spring 2021, Spring 2022 — Principles of Programming Languages
• Fall 2020, Fall 2021 — Formal Verification (Course website on Canvas)
• Spring 2020 — CSCI-2244 Randomness and Computation (Course website on Canvas)
• Fall 2019 — CSCI-2244 Randomness and Computation

Support

My work is supported by NSF grants 2035314, 2106559, 2123842, and a gift from Oracle Labs.

Notes

• Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms
  J. Tassarotti
  Draft 2017 [.pdf] [arXiv]