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 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've written several verified systems, where we wrote a specification of what the system should do, then used the Coq proof assistant to prove that the implementation meets the specification. So far my work has centered around a theme of storage systems, including a verified file system (FSCQ) and 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.