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 implemented and checked using 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 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.
