Tej Chajed
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
17
Venues
7
Active years
2013–2025
Best venue rank
A*
Where they publish
Papers
17 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | OSDI | Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. | Tony Nuda Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, Bryan Parno |
| 2024 | CAV | Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas. | Eden Frenkel, Tej Chajed, Oded Padon, Sharon Shoham |
| 2024 | OSDI | Anvil: Verifying Liveness of Cluster Management Controllers. | Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, Tianyin Xu |
| 2024 | OSDI | Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. | Tony Nuda Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, Bryan Parno |
| 2024 | SOSP | Verus: A Practical Foundation for Systems Verification. | 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 | HotOS | Beyond isolation: OS verification as a foundation for correct applications. | Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, Andrea Lattuada |
| 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 | OSDI | GoJournal: a verified, concurrent, crash-safe journaling system. | Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, Nickolai Zeldovich |
| 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 | OSDI | Verifying concurrent software using movers in CSPEC. | Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, Nickolai Zeldovich |
| 2018 | OSDI | Proving confidentiality in a file system using DiskSec. | Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2017 | SOSP | Verifying a high-performance crash-safe file system using a tree specification. | Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2016 | USENIX | Using Crash Hoare Logic for Certifying the FSCQ File System. | Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2015 | HotOS | Amber: Decoupling User Data from Web Applications. | Tej Chajed, Jon Gjengset, Jelle van den Hooff, M. Frans Kaashoek, James Mickens, Robert Morris, Nickolai Zeldovich |
| 2015 | SOSP | Using Crash Hoare logic for certifying the FSCQ file system. | Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2013 | CLOUD | 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 |