Joseph Tassarotti

61 papers A* 14A 2B 2Misc 1Journal 39Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs.
Proc. ACM Program. Lang.
Alexandre Moine, Sam Westrick, Joseph Tassarotti
2026 J jnl
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants.
Proc. ACM Program. Lang.
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
2025 J jnl
A Demonic Outcome Logic for Randomized Nondeterminism.
Proc. ACM Program. Lang.
Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti
2025 J jnl
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs.
CoRR
Alexandre Moine, Sam Westrick, Joseph Tassarotti
2025 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2025 A* conf
Logical Relations for Formally Verified Authenticated Data Structures.
CCS
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
2025 J jnl
Logical Relations for Formally Verified Authenticated Data Structures.
CoRR
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
Proc. ACM Program. Lang.
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2025 A* conf
ParserHawk: Hardware-aware parser generator using program synthesis.
SIGCOMM
Xiangyu Gao, Jiaqi Gao, Karan Kumar G., Muhammad Haseeb, Ennan Zhai, Bili Dong, Joseph Tassarotti, Srinivas Narayana, Anirudh Sivaraman
2025 J jnl
Verified Foundations for Differential Privacy.
Proc. ACM Program. Lang.
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan
2024 J jnl
A Demonic Outcome Logic for Randomized Nondeterminism.
CoRR
Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
CoRR
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 A* conf
Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation.
SOSP
Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti, Nickolai Zeldovich
2024 J jnl
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants.
CoRR
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Verified Foundations for Differential Privacy.
CoRR
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan
2024 J jnl
Verified Foundations for Differential Privacy.
IACR Cryptol. ePrint Arch.
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan
2023 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2023 J jnl
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412).
Dagstuhl Reports
Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev
2023 J jnl
Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version).
CoRR
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2023 A* conf
Grove: a Separation-Logic Library for Verifying Distributed Systems.
SOSP
Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2023 — conf
The K2 Architecture for Trustworthy Hardware Security Modules.
KISV@SOSP
Anish Athalye, M. Frans Kaashoek, Nickolai Zeldovich, Joseph Tassarotti
2023 J jnl
Verified Density Compilation for a Probabilistic Programming Language.
Proc. ACM Program. Lang.
Joseph Tassarotti, Jean-Baptiste Tristan
2023 A* conf
Verifying vMVCC, a high-performance transaction library using multi-version concurrency control.
OSDI
Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2022 J jnl
A separation logic for negative dependence.
Proc. ACM Program. Lang.
Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti
2022 J jnl
Later credits: resourceful reasoning for the later modality.
Proc. ACM Program. Lang.
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2022 A* conf
Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning.
OSDI
Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, Nickolai Zeldovich
2021 J jnl
A Separation Logic for Negative Dependence.
CoRR
Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti
2021 B conf
A formal proof of PAC learnability for decision stumps.
CPP
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan
2021 A* conf
GoJournal: a verified, concurrent, crash-safe journaling system.
OSDI
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
2021 Misc conf
On Building Modular and Elastic Data Structures with Bulk Operations.
ICDCN
Kevin Williams, Joe Foster, Athicha Srivirote, Ahmed Hassan, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
2021 A* conf
Rabia: Simplifying State-Machine Replication Through Randomization.
SOSP
Haochen Pan, Jesse Tuglu, Neo Zhou, Tianshu Wang, Yicheng Shen, Xiong Zheng, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
2021 J jnl
Rabia: Simplifying State-Machine Replication Through Randomization.
CoRR
Haochen Pan, Jesse Tuglu, Neo Zhou, Tianshu Wang, Yicheng Shen, Xiong Zheng, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri
2021 A* conf
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
PLDI
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2020 J jnl
Verification of ML Systems via Reparameterization.
CoRR
Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, Anindya Banerjee
2019 J jnl
A Formal Proof of PAC Learnability for Decision Stumps.
CoRR
Joseph Tassarotti, Jean-Baptiste Tristan, Koundinya Vajjha
2019 J jnl
A separation logic for concurrent randomized programs.
Proc. ACM Program. Lang.
Joseph Tassarotti, Robert Harper
2019 A* conf
Argosy: verifying layered storage systems with recovery refinement.
PLDI
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2019 — conf
Scaling Hierarchical Coreference with Homomorphic Compression.
AKBC
Michael L. Wick, Swetasudha Panda, Joseph Tassarotti, Jean-Baptiste Tristan
2019 A conf
Sketching for Latent Dirichlet-Categorical Models.
AISTATS
Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick
2019 A* conf
Verifying concurrent, crash-safe systems with Perennial.
SOSP
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2018 J jnl
A Separation Logic for Concurrent Randomized Programs.
CoRR
Joseph Tassarotti, Robert Harper
2018 J jnl
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang.
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018 J jnl
Sketching for Latent Dirichlet-Categorical Models.
CoRR
Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick
2018 B conf
Verified Tail Bounds for Randomized Programs.
ITP
Joseph Tassarotti, Robert Harper
2017 A conf
A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
ESOP
Joseph Tassarotti, Ralf Jung, Robert Harper
2017 J jnl
A Higher-Order Logic for Concurrent Termination-Preserving Refinement.
CoRR
Joseph Tassarotti, Ralf Jung, Robert Harper
2017 J jnl
Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms.
CoRR
Joseph Tassarotti
2015 A* conf
Efficient Training of LDA on a GPU by Mean-for-Mode Estimation.
ICML
Jean-Baptiste Tristan, Joseph Tassarotti, Guy L. Steele Jr.
2015 A* conf
Verifying read-copy-update in a logic for weak memory.
PLDI
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
2014 — conf
Augur: Data-Parallel Probabilistic Modeling.
NIPS
Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.
2013 J jnl
Augur: a Modeling Language for Data-Parallel Probabilistic Inference.
CoRR
Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.
2012 A* conf
RockSalt: better, faster, stronger SFI for the x86.
PLDI
Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan