Natjam: design and evaluation of eviction policies for supporting priorities and deadlines in mapreduce clusters. - Brian Cho; Muntasir Raihan Rahman; Tej Chajed; Indranil Gupta; Cristina L. Abad; Nathan Roberts; Philbert Lin (SoCC, 2013)

Amber: Decoupling User Data from Web Applications. - Tej Chajed; Jon Gjengset; Jelle van den Hooff; M. Frans Kaashoek; James Mickens; Robert Morris 005; Nickolai Zeldovich (HotOS, 2015)

Using Crash Hoare Logic for Certifying the FSCQ File System. - Haogang Chen 001; Daniel Ziegler 002; Tej Chajed; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (USENIX ATC, 2016)

Verifying a high-performance crash-safe file system using a tree specification. - Haogang Chen 001; Tej Chajed; Alex Konradi; Stephanie Wang; Atalay Mert Ileri; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2017)

Certifying a file system using crash hoare logic: correctness in the presence of crashes. - Tej Chajed; Haogang Chen 001; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich; Daniel Ziegler 002 (Commun. ACM, 2017)

Verifying concurrent software using movers in CSPEC. - Tej Chajed; M. Frans Kaashoek; Butler W. Lampson; Nickolai Zeldovich (OSDI, 2018)

Proving confidentiality in a file system using DiskSec. - Atalay Mert Ileri; Tej Chajed; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2018)

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)

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. - Tahina Ramananandro; Antoine Delignat-Lavaud; Cédric Fournet; Nikhil Swamy; Tej Chajed; Nadim Kobeissi; Jonathan Protzenko (USENIX Security Symposium, 2019)

GoJournal: a verified, concurrent, crash-safe journaling system. - Tej Chajed; Joseph Tassarotti; Mark Theng; Ralf Jung 002; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 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)

Verifying a concurrent, crash-safe file system with sequential reasoning - Tej Chajed (2022)

Beyond isolation: OS verification as a foundation for correct applications. - Matthias Brun 002; Reto Achermann; Tej Chajed; Jon Howell; Gerd Zellweger; Andrea Lattuada 001 (HotOS, 2023)

DBSP: Automatic Incremental View Maintenance for Rich Query Languages. - Mihai Budiu; Tej Chajed; Frank McSherry; Leonid Ryzhyk; Val Tannen (Proc. VLDB Endow., 2023)

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. - Eden Frenkel; Tej Chajed; Oded Padon; Sharon Shoham (CAV (2), 2024)

Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative Execution. - Jing Liu 074; Xiangpeng Hao; Andrea C. Arpaci-Dusseau; Remzi H. Arpaci-Dusseau; Tej Chajed (HotStorage, 2024)

Anvil: Verifying Liveness of Cluster Management Controllers. - Xudong Sun 013; Wenjie Ma; Jiawei Tyler Gu; Zicheng Ma; Tej Chajed; Jon Howell; Andrea Lattuada 001; Oded Padon; Lalith Suresh 001; Adriana Szekeres; Tianyin Xu (OSDI, 2024)

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. - Tony Nuda Zhang; Travis Hance; Manos Kapritsos; Tej Chajed; Bryan Parno (OSDI, 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

DBSP: Incremental Computation on Streams and Its Applications to Databases. - Mihai Budiu; Tej Chajed; Frank McSherry; Leonid Ryzhyk; Val Tannen (SIGMOD Rec., 2024)

Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. - Tony Nuda Zhang; Keshav Singh; Tej Chajed; Manos Kapritsos; Bryan Parno (OSDI, 2025)

DBSP: automatic incremental view maintenance for rich query languages. - Mihai Budiu; Leonid Ryzhyk; Gerd Zellweger; Ben Pfaff; Lalith Suresh 001; Simon Kassing; Abhinav Gyawali; Matei Budiu; Tej Chajed; Frank McSherry; Val Tannen (VLDB J., 2025)