I am a graduate student at Massachusetts Institute of Technology. Before coming here, I was an undergraduate at the Indian Institute of Technology, Madras. Madras (now renamed Chennai) is also the city I grew up in.
I am interested in formal verification of distributed systems and hardware systems using proof assistants, high-level languages which combine verification and design, and computer architecture. My advisor is Professor Arvind, and I work in CSAIL. Recently, I've worked on establishing the equivalence between the operational semantics of hardware systems and axiomatic memory model specifications that programmers normally use to determine behavior of programs. I've also worked on proving the correctness of cache coherence protocols for a multi-level cache hierarchy using the Coq Theorem prover.
[pdf]
[pdf]
Arvind Nirav Dave Asif Khan Silas Boyd-Wickizer Michael Pellauer Michael Adler Joel Emer Alfred Man Cheuk Ng Abhinav Agarwal Kermin Elliott Fleming Jamey Hicks Myron King Gopal Raghavan Adam Chlipala Michal Karczmarek
Distributed Modular Hardware Compilation of Guarded Atomic Actions and 2013 MEMOCODE papers/modularbsv.pdf A new synthesis procedure for atomic rules containing multi-cycle function blocks and 2014 MEMOCODE (accepted) papers/multicycle.pdf Fast and cycle-accurate modeling of a multicore processor , and 2012 ISPASS papers/ppcIspass.pdf A general technique for deterministic model-cycle-level debugging and 2012 MEMOCODE papers/ppcMemocode.pdf A-Port Networks: Preserving the Timed Behavior of Synchronous Systems for Modeling on FPGAs , , and 2009 TRETS papers/aportsJournal.pdf Bounded Dataflow Networks and Latency-Insensitive circuits 2009 MEMOCODE papers/libdns.pdf A-Ports: an efficient abstraction for cycle-accurate performance models on FPGAs , , and 2008 FPGA papers/aports-fpga.pdf Quick Performance Models Quickly: Closely-Coupled Partitioned Simulation on FPGAs , , and 2008 ISPASS papers/aports-ispass.pdf From WiFi to WiMAX: Techniques for High-Level IP Reuse across Different OFDM Protocols , , , and 2007 MEMOCODE papers/airblue.pdf
Address:
Computer Science and Artificial Intelligence Lab
The Stata Center
Massachusetts Institute of Technology
32 Vassar Street, 32-G836
Cambridge, MA 02139

Email: {first_character_of_my_last_name}{first_six_characters_of_my_first_name} at csail dot mit dot edu