Email: joseph.tassarotti@bc.edu
CV (November 2021)

I'm an assistant professor in the Computer Science Department at Boston College. 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, where I retain a research affiliate position.

Teaching

• 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

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 (conditionally accepted)


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

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]