Joseph Tassarotti
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
20
Venues
12
Active years
2012–2026
Best venue rank
A*
Where they publish
Papers
20 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | LICS | Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic. | Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti |
| 2025 | CCS | Logical Relations for Formally Verified Authenticated Data Structures. | Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti |
| 2025 | SIGCOMM | ParserHawk: Hardware-aware parser generator using program synthesis. | Xiangyu Gao, Jiaqi Gao, Karan Kumar G., Muhammad Haseeb, Ennan Zhai, Bili Dong, Joseph Tassarotti, Srinivas Narayana, Anirudh Sivaraman |
| 2024 | SOSP | 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 |
| 2023 | OSDI | 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 |
| 2023 | SOSP | Grove: a Separation-Logic Library for Verifying Distributed Systems. | Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich |
| 2022 | OSDI | Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. | Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, Nickolai Zeldovich |
| 2021 | CPP | A formal proof of PAC learnability for decision stumps. | Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan |
| 2021 | ICDCN | On Building Modular and Elastic Data Structures with Bulk Operations. | Kevin Williams, Joe Foster, Athicha Srivirote, Ahmed Hassan, Joseph Tassarotti, Lewis Tseng, Roberto Palmieri |
| 2021 | OSDI | GoJournal: a verified, concurrent, crash-safe journaling system. | Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich |
| 2021 | PLDI | Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. | Simon Spies, Lennard Gher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal |
| 2021 | SOSP | 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 |
| 2019 | AISTATS | Sketching for Latent Dirichlet-Categorical Models. | Joseph Tassarotti, Jean-Baptiste Tristan, Michael L. Wick |
| 2019 | PLDI | Argosy: verifying layered storage systems with recovery refinement. | Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich |
| 2019 | SOSP | Verifying concurrent, crash-safe systems with Perennial. | Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich |
| 2018 | ITP | Verified Tail Bounds for Randomized Programs. | Joseph Tassarotti, Robert Harper |
| 2017 | ESOP | A Higher-Order Logic for Concurrent Termination-Preserving Refinement. | Joseph Tassarotti, Ralf Jung, Robert Harper |
| 2015 | ICML | Efficient Training of LDA on a GPU by Mean-for-Mode Estimation. | Jean-Baptiste Tristan, Joseph Tassarotti, Guy L. Steele Jr. |
| 2015 | PLDI | Verifying read-copy-update in a logic for weak memory. | Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis |
| 2012 | PLDI | RockSalt: better, faster, stronger SFI for the x86. | Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan |