Tej Chajed

I'm Tej Chajed, a final-year PhD student in PDOS at MIT CSAIL, advised by Frans Kaashoek and Nickolai Zeldovich. I work on formal verification of systems software — I implement systems and prove they do what they're supposed to.

Before coming to MIT I was at UIUC, where I got undergraduate degrees in Electrical Engineering and Computer Science.

I am on the faculty job market this year. You can find my research statement, teaching statement, and CV here.

Tej Chajed picture

Research

Even critical systems software has bugs — for example, file systems have bugs that occasionally lead to users losing data. My research aims to write systems software that always does what it's supposed to. We do this with formal verification: we write a precise specification of what the system is supposed to do and prove that the implementation meets the specification. My research has culminated in DaisyNFS, a verified, concurrent file system that gets good performance. The path to verifying DaisyNFS involved developing new frameworks and tools, including Perennial, a framework for reasoning about crash safety and concurrency, and Goose, a system for connecting the proofs to Go code.

I do a lot of work on Coq-related things, including maintaining a list of Coq tricks for the advanced user and contributing to Iris.

I'm a communication Fellow in the EECS Communication Lab, where I help students with technical communication. If you're working on something where you think I could help, please reach out! I'm particularly excited about working on research papers and conference presentations.

Ph.D. thesis

Verifying a concurrent, crash-safe file system with sequential reasoning (Ph.D. thesis, MIT, May 2022)
 
Tej Chajed

Publications

Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning   (conditionally accepted to OSDI 2022)
Tej Chajed, Joseph Tassarotti, Mark Theng, M. Frans Kaashoek, and Nickolai Zeldovich
GoJournal: a verified, concurrent, crash-safe journaling system   (OSDI 2021)
Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich
Record Updates in Coq   (CoqPL 2021)
Tej Chajed
Verifying concurrent Go code in Coq with Goose   (CoqPL 2020)
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich
Verifying concurrent, crash-safe systems with Perennial   (SOSP 2019)
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich
EverParse: Verified Secure Zero-Copy Parsers for
Authenticated Message Formats
  (USENIX Security 2019)
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko
Argosy: Verifying Layered Storage Systems with Recovery Refinement   (PLDI 2019)
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich
Verifying concurrent software using movers in CSPEC   (OSDI 2018)
Tej Chajed, M. Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich
Proving confidentiality in a file system using DiskSec   (OSDI 2018)
Atalay İleri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
Verifying a high-performance crash-safe file system
using a tree specification
  (SOSP 2017)
Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
Extending a verified file system with concurrency   (SOSP 2017 SRC)
Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
Certifying a file system using Crash Hoare Logic:
Correctness in the presence of crashes
  (CACM 2017)
Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, and Daniel Ziegler
Using Crash Hoare Logic for certifying the FSCQ file system   (SOSP 2015)
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
Amber: Decoupling user data from web applications   (HotOS 2015)
Tej Chajed, Jon Gjengset, Jelle van den Hooff, M. Frans Kaashoek, James Mickens, Robert Morris, and Nickolai Zeldovich

Teaching

I helped create 6.826 (Principles of Computer Systems), a class on systems verification, and in particular I created the lab assignments. I was a TA for the class in Fall 2020, Fall 2019, and Fall 2017.

Service

During my PhD I served on a conference program committee for PLDI 2022 and several artifact evaluation committees (AECs).

How to pronounce my name

"Tej" rhymes with "page", and Chajed is pronounced as written (CHA-jed).