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]