Joseph Tassarotti

According to our database, Joseph Tassarotti authored at least 31 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

2023

Verified Density Compilation for a Probabilistic Programming Language.

Joseph Tassarotti, Jean-Baptiste Tristan

Proc. ACM Program. Lang., 2023

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412).

Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev

Dagstuhl Reports, 2023

Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version).

Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

CoRR, 2023

Grove: a Separation-Logic Library for Verifying Distributed Systems.

Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 29th Symposium on Operating Systems Principles, 2023

Verifying vMVCC, a high-performance transaction library using multi-version concurrency control.

Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

The K2 Architecture for Trustworthy Hardware Security Modules.

Anish Athalye, M. Frans Kaashoek, Nickolai Zeldovich, Joseph Tassarotti

Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, 2023

2022

Later credits: resourceful reasoning for the later modality.

Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Proc. ACM Program. Lang., 2022

A separation logic for negative dependence.

Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti

Proc. ACM Program. Lang., 2022

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning.

Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

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

Proceedings of the SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, 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

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

GoJournal: a verified, concurrent, crash-safe journaling system.

Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 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

Proceedings of the ICDCN '21: International Conference on Distributed Computing and Networking, 2021

A formal proof of PAC learnability for decision stumps.

Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Verification of ML Systems via Reparameterization.

Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, Anindya Banerjee

CoRR, 2020

2019

A separation logic for concurrent randomized programs.

Joseph Tassarotti, Robert Harper

Proc. ACM Program. Lang., 2019

A Formal Proof of PAC Learnability for Decision Stumps.

Joseph Tassarotti, Jean-Baptiste Tristan, Koundinya Vajjha

CoRR, 2019

Verifying concurrent, crash-safe systems with Perennial.

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Argosy: verifying layered storage systems with recovery refinement.

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Scaling Hierarchical Coreference with Homomorphic Compression.

Michael L. Wick, Swetasudha Panda, Joseph Tassarotti, Jean-Baptiste Tristan

Proceedings of the 1st Conference on Automated Knowledge Base Construction, 2019

Sketching for Latent Dirichlet-Categorical Models.

Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick

Proceedings of the 22nd International Conference on Artificial Intelligence and Statistics, 2019

2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer

Proc. ACM Program. Lang., 2018

Verified Tail Bounds for Randomized Programs.

Joseph Tassarotti, Robert Harper

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Probabilistic Recurrence Relations for Work and Span of Parallel Algorithms.

Joseph Tassarotti

CoRR, 2017

A Higher-Order Logic for Concurrent Termination-Preserving Refinement.

Joseph Tassarotti, Ralf Jung, Robert Harper

Proceedings of the Programming Languages and Systems, 2017

2015

Verifying read-copy-update in a logic for weak memory.

Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Efficient Training of LDA on a GPU by Mean-for-Mode Estimation.

Jean-Baptiste Tristan, Joseph Tassarotti, Guy L. Steele Jr.

Proceedings of the 32nd International Conference on Machine Learning, 2015

2014

Augur: Data-Parallel Probabilistic Modeling.

Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.

Proceedings of the Advances in Neural Information Processing Systems 27: Annual Conference on Neural Information Processing Systems 2014, 2014

2013

Augur: a Modeling Language for Data-Parallel Probabilistic Inference.

Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam Craig Pocock, Stephen J. Green, Guy L. Steele Jr.

CoRR, 2013

2012

RockSalt: better, faster, stronger SFI for the x86.

Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012