Tej Chajed

25 papers A* 13A 2Journal 5Unranked 4
YearRankTypeTitle / Venue / Authors
2025 A* conf
Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols.
OSDI
Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, Bryan Parno
2025 J jnl
DBSP: automatic incremental view maintenance for rich query languages.
VLDB J.
Mihai Budiu, Leonid Ryzhyk, Gerd Zellweger, Ben Pfaff, Lalith Suresh, Simon Kassing, Abhinav Gyawali, Matei Budiu, Tej Chajed, Frank McSherry, Val Tannen
2024 A* conf
Anvil: Verifying Liveness of Cluster Management Controllers.
OSDI
Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, Tianyin Xu
2024 J jnl
DBSP: Incremental Computation on Streams and Its Applications to Databases.
SIGMOD Rec.
Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, Val Tannen
2024 — conf
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CAV (2)
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 J jnl
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas.
CoRR
Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham
2024 A* conf
Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs.
OSDI
Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, Bryan Parno
2024 — conf
Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative Execution.
HotStorage
Jing Liu, Xiangpeng Hao, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, Tej Chajed
2024 A* conf
Verus: A Practical Foundation for Systems Verification.
SOSP
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, Bryan Parno
2023 A conf
Beyond isolation: OS verification as a foundation for correct applications.
HotOS
Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, Andrea Lattuada
2023 J jnl
DBSP: Automatic Incremental View Maintenance for Rich Query Languages.
Proc. VLDB Endow.
Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, Val Tannen
2022 — —
Verifying a concurrent, crash-safe file system with sequential reasoning
Tej Chajed
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 A* conf
GoJournal: a verified, concurrent, crash-safe journaling system.
OSDI
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich
2019 A* conf
Argosy: verifying layered storage systems with recovery refinement.
PLDI
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2019 A* conf
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
USENIX Security Symposium
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
2019 A* conf
Verifying concurrent, crash-safe systems with Perennial.
SOSP
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich
2018 A* conf
Proving confidentiality in a file system using DiskSec.
OSDI
Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2018 A* conf
Verifying concurrent software using movers in CSPEC.
OSDI
Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, Nickolai Zeldovich
2017 J jnl
Certifying a file system using crash hoare logic: correctness in the presence of crashes.
Commun. ACM
Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, Daniel Ziegler
2017 A* conf
Verifying a high-performance crash-safe file system using a tree specification.
SOSP
Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2016 — conf
Using Crash Hoare Logic for Certifying the FSCQ File System.
USENIX ATC
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2015 A conf
Amber: Decoupling User Data from Web Applications.
HotOS
Tej Chajed, Jon Gjengset, Jelle van den Hooff, M. Frans Kaashoek, James Mickens, Robert Morris, Nickolai Zeldovich
2015 A* conf
Using Crash Hoare logic for certifying the FSCQ file system.
SOSP
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
2013 — conf
Natjam: design and evaluation of eviction policies for supporting priorities and deadlines in mapreduce clusters.
SoCC
Brian Cho, Muntasir Raihan Rahman, Tej Chajed, Indranil Gupta, Cristina L. Abad, Nathan Roberts, Philbert Lin