I'm Tej Chajed, a recent PhD graduate from the PDOS group at MIT, 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'm excited to join the University of Wisconsin-Madison as an assistant professor in Fall 2023! Before starting I'll be at VMware Research for a one-year postdoc.
In case you're interested, you can find my research statement, teaching statement, and CV from my faculty application materials.
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.