I'm Tej Chajed, a sixth-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.
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. These proofs are carried out on a computer with the Coq proof assistant, giving us high assurance that the proofs are correct. So far my work has centered around a theme of storage systems and concurrency, including a verified file system (FSCQ) and Perennial, a framework that combines concurrency and crash-safety reasoning.
I do a lot of work on Coq-related things, including maintaining a list of Coq tricks for the advanced user.
I'm an advisor 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.
