Name:Yatin Manerkar

Bio:

I am an incoming Assistant Professor in the Computer Science and Engineering (CSE) Department at the University of Michigan beginning Fall 2021. I recently completed my PhD in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. I am currently doing a “pre-battical” postdoc with Prof. Sanjit Seshia at UC Berkeley in between graduation and starting at Michigan.

My research lies on the boundary between computer architecture and formal methods, and focuses on developing automated formal methodologies and tools for the design and verification of computing systems. My work spans the hardware/software stack, from high-level programming languages down to low-level Verilog circuits. During my PhD, my research focused on the verification of memory consistency model (MCM) properties in parallel hardware and software. MCMs specify the ordering rules for memory operations used for communication and synchronization in shared-memory parallel programs, so MCM verification is critical to parallel system correctness. My work has found real-world bugs in C++ compilers, an open-source processor implementation in Verilog, and in the widely-used RISC-V instruction set (ISA). My work has also enriched the formal methods community by developing new formal analysis techniques.

Before joining Princeton, I completed my BASc in Computer Engineering at the University of Waterloo and a M.S. in Computer Science and Engineering at the University of Michigan. I also worked full-time at Qualcomm Research for one year.

Country:United States

Affiliation:University of Michigan and UC Berkeley

Research interests:Formal verification, computer architecture, memory consistency models, cache coherence, ethical AI