Joseph Tassarotti

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 36

Top Topics

Decision Stumps

Distributed Systems

Probabilistic Modeling

Top Venues

Proc. ACM Program. Lang.

Publications

Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. CoRR (2024)
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Approximate Relational Reasoning for Higher-Order Probabilistic Programs. CoRR (2024)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Almost-Sure Termination by Guarded Refinement. CoRR (2024)
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. CoRR (2024)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8 (POPL) (2024)
Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. OSDI (2023)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Grove: a Separation-Logic Library for Verifying Distributed Systems. SOSP (2023)
Anish Athalye, M. Frans Kaashoek, Nickolai Zeldovich, Joseph Tassarotti
The K2 Architecture for Trustworthy Hardware Security Modules. KISV@SOSP (2023)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. CoRR (2023)
Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). Dagstuhl Reports 13 (10) (2023)
Joseph Tassarotti, Jean-Baptiste Tristan
Verified Density Compilation for a Probabilistic Programming Language. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version). CoRR (2023)
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, Nickolai Zeldovich
Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. OSDI (2022)
Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti
A separation logic for negative dependence. Proc. ACM Program. Lang. 6 (POPL) (2022)
Haochen Pan, Jesse Tuglu, Neo Zhou, Tianshu Wang, Yicheng Shen, Xiong Zheng, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
Rabia: Simplifying State-Machine Replication Through Randomization. SOSP (2021)
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI (2021)
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan
A formal proof of PAC learnability for decision stumps. CPP (2021)
Haochen Pan, Jesse Tuglu, Neo Zhou, Tianshu Wang, Yicheng Shen, Xiong Zheng, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
Rabia: Simplifying State-Machine Replication Through Randomization. CoRR (2021)
Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti
A Separation Logic for Negative Dependence. CoRR (2021)
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
GoJournal: a verified, concurrent, crash-safe journaling system. OSDI (2021)
Kevin Williams, Joe Foster, Athicha Srivirote, Ahmed Hassan, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
On Building Modular and Elastic Data Structures with Bulk Operations. ICDCN (2021)
Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, Anindya Banerjee
Verification of ML Systems via Reparameterization. CoRR (2020)
Joseph Tassarotti, Robert Harper
A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3 (POPL) (2019)
Joseph Tassarotti, Jean-Baptiste Tristan, Koundinya Vajjha
A Formal Proof of PAC Learnability for Decision Stumps. CoRR (2019)
Michael L. Wick, Swetasudha Panda, Joseph Tassarotti, Jean-Baptiste Tristan
Scaling Hierarchical Coreference with Homomorphic Compression. AKBC (2019)
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Verifying concurrent, crash-safe systems with Perennial. SOSP (2019)
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
Argosy: verifying layered storage systems with recovery refinement. PLDI (2019)
Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick
Sketching for Latent Dirichlet-Categorical Models. AISTATS (2019)
Joseph Tassarotti, Robert Harper
Verified Tail Bounds for Randomized Programs. ITP (2018)
Joseph Tassarotti, Robert Harper
A Separation Logic for Concurrent Randomized Programs. CoRR (2018)
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick
Sketching for Latent Dirichlet-Categorical Models. CoRR (2018)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. ESOP (2017)
Joseph Tassarotti, Ralf Jung, Robert Harper
A Higher-Order Logic for Concurrent Termination-Preserving Refinement. CoRR (2017)
Joseph Tassarotti
Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms. CoRR (2017)
Jean-Baptiste Tristan, Joseph Tassarotti, Guy L. Steele Jr.
Efficient Training of LDA on a GPU by Mean-for-Mode Estimation. ICML (2015)
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
Verifying read-copy-update in a logic for weak memory. PLDI (2015)
Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.
Augur: Data-Parallel Probabilistic Modeling. NIPS (2014)
Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.
Augur: a Modeling Language for Data-Parallel Probabilistic Inference. CoRR (2013)
Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan
RockSalt: better, faster, stronger SFI for the x86. PLDI (2012)