Tej Chajed

tchajed@mit.edu

Hello! I'm Tej Chajed, a fifth-year PhD student in PDOS at MIT CSAIL, advised by Frans Kaashoek and Nickolai Zeldovich. I work on formal verification of systems - I implement systems and prove that they're correct.

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

Tej Chajed picture

Research

In my research I develop new techniques for writing verified systems software. For each system, we use the Coq proof assistant to write a specification, implement the system, and write a machine-checked proof that the implementation meets the specification. Every system is also an exploration in new techniques for systems verification. My work so far has centered around a theme of storage systems, especially work on the FSCQ verified file system, and on concurrency.

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

Publications

Verifying concurrent software using movers in CSPEC   (OSDI 2018)
Tej Chajed, M. Frans Kaashoek, Butler Lampson, and and Nickolai Zeldovich
Proving confidentiality in a file system using DiskSec   (OSDI 2018)
Atalay Ileri, 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 Ileri, 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
Extending a verified file system with concurrency   (SOSP 2017 SRC)
Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
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