RockSalt: better, faster, stronger SFI for the x86. - Greg Morrisett; Gang Tan; Joseph Tassarotti; Jean-Baptiste Tristan; Edward Gan (PLDI, 2012)

Augur: a Modeling Language for Data-Parallel Probabilistic Inference. - Jean-Baptiste Tristan; Daniel Huang 001; Joseph Tassarotti; Adam Craig Pocock; Stephen J. Green; Guy L. Steele Jr. (CoRR, 2013)

Augur: Data-Parallel Probabilistic Modeling. - Jean-Baptiste Tristan; Daniel Huang 001; Joseph Tassarotti; Adam Craig Pocock; Stephen J. Green; Guy L. Steele Jr. (NIPS, 2014)

Efficient Training of LDA on a GPU by Mean-for-Mode Estimation. - Jean-Baptiste Tristan; Joseph Tassarotti; Guy L. Steele Jr. (ICML, 2015)

Verifying read-copy-update in a logic for weak memory. - Joseph Tassarotti; Derek Dreyer; Viktor Vafeiadis (PLDI, 2015)

A Higher-Order Logic for Concurrent Termination-Preserving Refinement. - Joseph Tassarotti; Ralf Jung 002; Robert Harper 001 (ESOP, 2017)

Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms. - Joseph Tassarotti (CoRR, 2017)

Verified Tail Bounds for Randomized Programs. - Joseph Tassarotti; Robert Harper 001 (ITP, 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Sketching for Latent Dirichlet-Categorical Models. - Joseph Tassarotti; Jean-Baptiste Tristan; Michael L. Wick (AISTATS, 2019)

Scaling Hierarchical Coreference with Homomorphic Compression. - Michael L. Wick; Swetasudha Panda; Joseph Tassarotti; Jean-Baptiste Tristan (AKBC, 2019)

Argosy: verifying layered storage systems with recovery refinement. - Tej Chajed; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (PLDI, 2019)

Verifying concurrent, crash-safe systems with Perennial. - Tej Chajed; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2019)

A Formal Proof of PAC Learnability for Decision Stumps. - Joseph Tassarotti; Jean-Baptiste Tristan; Koundinya Vajjha (CoRR, 2019)

A separation logic for concurrent randomized programs. - Joseph Tassarotti; Robert Harper 001 (Proc. ACM Program. Lang., 2019)

Verification of ML Systems via Reparameterization. - Jean-Baptiste Tristan; Joseph Tassarotti; Koundinya Vajjha; Michael L. Wick; Anindya Banerjee 001 (CoRR, 2020)

A formal proof of PAC learnability for decision stumps. - Joseph Tassarotti; Koundinya Vajjha; Anindya Banerjee 001; Jean-Baptiste Tristan (CPP, 2021)

On Building Modular and Elastic Data Structures with Bulk Operations. - Kevin Williams; Joe Foster; Athicha Srivirote; Ahmed Hassan; Joseph Tassarotti; Lewis Tseng; Roberto Palmieri (ICDCN, 2021)

GoJournal: a verified, concurrent, crash-safe journaling system. - Tej Chajed; Joseph Tassarotti; Mark Theng; Ralf Jung 002; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2021)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Rabia: Simplifying State-Machine Replication Through Randomization. - Haochen Pan; Jesse Tuglu; Neo Zhou; Tianshu Wang; Yicheng Shen; Xiong Zheng; Joseph Tassarotti; Lewis Tseng; Roberto Palmieri (SOSP, 2021)

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. - Tej Chajed; Joseph Tassarotti; Mark Theng; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2022)

A separation logic for negative dependence. - Jialu Bao; Marco Gaboardi; Justin Hsu; Joseph Tassarotti (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

The K2 Architecture for Trustworthy Hardware Security Modules. - Anish Athalye; M. Frans Kaashoek; Nickolai Zeldovich; Joseph Tassarotti (KISV@SOSP, 2023)

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. - Yun-Sheng Chang; Ralf Jung 002; Upamanyu Sharma; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems. - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2023)

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version). - Upamanyu Sharma; Ralf Jung 002; Joseph Tassarotti; M. Frans Kaashoek; Nickolai Zeldovich (CoRR, 2023)

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). - Ori Lahav 001; Azalea Raad; Joseph Tassarotti; Viktor Vafeiadis; Anton Podkopaev (Dagstuhl Reports, 2023)

Verified Density Compilation for a Probabilistic Programming Language. - Joseph Tassarotti; Jean-Baptiste Tristan (Proc. ACM Program. Lang., 2023)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2023)

Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. - Anish Athalye; Henry Corrigan-Gibbs; M. Frans Kaashoek; Joseph Tassarotti; Nickolai Zeldovich (SOSP, 2024)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants. - Noam Zilberstein; Alexandra Silva 001; Joseph Tassarotti (CoRR, 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Almost-Sure Termination by Guarded Refinement. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs. - Philipp G. Haselwarter; Kwing Hei Li; Markus de Medeiros; Simon Oddershede Gregersen; Alejandro Aguirre 001; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Almost-Sure Termination by Guarded Refinement - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Verified Foundations for Differential Privacy. - Markus de Medeiros; Muhammad Naveed; Tancrède Lepoint; Temesghen Kahsai; Tristan Ravitch; Stefan Zetzsche; Anjali Joshi; Joseph Tassarotti; Aws Albarghouthi; Jean-Baptiste Tristan (Proc. ACM Program. Lang., 2025)

A Demonic Outcome Logic for Randomized Nondeterminism. - Noam Zilberstein; Dexter Kozen; Alexandra Silva 001; Joseph Tassarotti (Proc. ACM Program. Lang., 2025)

Logical Relations for Formally Verified Authenticated Data Structures. - Simon Oddershede Gregersen; Chaitanya Agarwal; Joseph Tassarotti (CoRR, 2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. - Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (CoRR, 2025)