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.
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.
