Profile picture

I am an Assistant Professor in the Computer Science and Engineering (CSE) Department at the University of Michigan. I recently completed my PhD in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. I was a postdoctoral researcher with Prof. Sanjit Seshia at UC Berkeley in between graduation and starting at Michigan.

I am hiring PhD students! If my research interests you, then please apply to Michigan's PhD program here and mention my name in your application. If you are a current U-M student interested in doing research with me, please send me email.

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.

I was a recipient of Princeton's Wallace Memorial Fellowship for the 2018-2019 academic year. The Wallace Memorial Fellowship is a Princeton Honorific Fellowship which provides funding to students displaying the highest scholarly excellence in graduate work during the year. I also received the 2019 Award for Excellence from Princeton's School of Engineering and Applied Sciences (SEAS).

I was selected to attend the 7th Heidelberg Laureate Forum (HLF) in September 2019. The HLF is an annual event where 200 young researchers in computer science and mathematics participate in a weeklong scientific exchange with recipients of the top awards in computing and mathematics (Turing Award, Abel Prize, Fields Medal, ACM Prize in Computing, and the Nevanlinna Prize).

My CV can be found here.

Research

Research Statement

We entrust large parts of our daily lives to computer systems, and these systems require thorough verification to ensure their correctness. System vulnerabilities can lead to leakage of confidential information, loss of money, and (in the case of cyber-physical systems) may even threaten one's physical safety and security. Many such bugs have in fact been found in computing systems in recent years, ranging from security vulnerabilities (like Meltdown and Spectre) to network errors to concurrency bugs.

Some important bugs are due to flaws in system design/specification, while others are due to implementations violating the design specification. Since verification is generally focused late in development, bugs tend to get caught late in development as well. Design bugs may necessitate a redesign, wasting the development time spent creating incorrect implementations. Furthermore, many bugs only occur in very specific scenarios, making them hard to find. Current verification processes have proven inadequate for catching these bugs, resulting in the release of flawed hardware and software.

Verification using formal methods provides strong correctness guarantees based on mathematical proofs, and is adept at catching hard-to-find bugs. My work aims to improve the verification of hardware and software using formal methods, without requiring engineers to have formal methods expertise. I propose a philosophy of Progressive Automated Formal Verification, i.e. verification throughout the system development process, from early-stage design through to final implementation. Progressive verification has multiple benefits, including reductions in verification overhead and in overall development time. Automating formal verification also enables engineering teams to prove strong correctness properties about their designs and implementations by themselves, shifting the verification burden away from the relatively small number of formal methods experts.

In progressive verification, formal models of systems are first created and verified during early-stage design, thus catching design bugs before implementation commences. These models can then evolve to become more detailed as system design progresses. Once the system is implemented, the implementation is formally verified against a proven-correct design model to help ensure implementation correctness. The number of steps in a progressive verification flow may vary depending on the type of system being built, but the key idea is to conduct verification throughout the design timeline and link the verification methods at each stage together.

The work in my dissertation constitutes a concrete instance of a progressive verification flow for MCM properties in parallel processors. However, progressive verification is a generic flow, and is applicable to other types of properties like hardware security properties. It is also applicable to other types of systems like cyber-physical systems.

Publications



Refereed Publications

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Aarti Gupta. PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. The 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2018.
    Nominated for best paper.
    Selected as a IEEE MICRO Top Picks Honorable Mention from the 2018 Computer Architecture Conferences.
    [PDF] [Slides] [Poster] [GitHub]

  • Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik. Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification. The 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2018.
    [PDF]

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "Full-Stack Memory Model Verification with TriCheck". IEEE Micro, 38 (3) (Top Picks of the 2017 Computer Architecture Conferences), May-June 2018.
    [PDF]

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. RTLCheck: Verifying the Memory Consistency of RTL Designs. The 50th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2017.
    Selected as a IEEE MICRO Top Picks Honorable Mention from the 2017 Computer Architecture Conferences.
    [PDF] [Slides] [Poster] [GitHub]

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. The 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2017.
    Selected as a IEEE MICRO Top Pick from the 2017 Computer Architecture Conferences.
    [PDF]

  • Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface. The 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015.
    Nominated for best paper.
    [PDF] [Slides] [Poster] [GitHub]

Non-Refereed Publications

  • Yatin A. Manerkar, Daniel Lustig, and Margaret Martonosi. RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification. CoRR abs/2003.04892, March 2020.
    [PDF]

  • Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs/1611.01507, November 2016.
    [PDF]

Thesis

  • Yatin A. Manerkar. Progressive Automated Formal Verification of Memory Consistency in Parallel Processors. PhD thesis, Princeton University, December 2020.
    [PDF]

Invited Talks



  • Why is Ethical AI hard? A Technical Perspective.
    Ethics of AI Learning Cohort, Princeton University, Princeton NJ, April 2021.

  • Progressive Automated Formal Verification of Hardware and Software Systems.
    University of Illinois Urbana-Champaign, Urbana IL, April 2020.
    Pennsylvania State University, State College PA, March 2020.
    Carnegie Mellon University, Pittsburgh PA, March 2020.
    University of Michigan, Ann Arbor MI, March 2020.
    Georgia Institute of Technology, Atlanta GA, February 2020.
    Rising Stars in Computer Architecture (RISC-A) Workshop, Atlanta GA, October 2019.

  • Automated Formal Memory Consistency Verification of Hardware.
    DeepSpec Workshop at PLDI 2019, Phoenix AZ. June 2019.
    [Slides]

  • Automated Formal Verification of Event Orderings in Parallel Hardware and Software.
    University of Toronto, Toronto ON, Canada, March 2019.

  • Automated Full-Stack Memory Model Verification with the Check Suite.
    Imperial College London, UK, July 2018.
    University of Cambridge, UK, July 2018.
    ARM Cambridge, UK, July 2018.
    [Slides]

  • C11 Compiler Mappings: Exploration, Verification, and Counterexamples.
    Dagstuhl Seminar 16471: Concurrency with Weak Memory Models. November 2016.
    [Slides]

Teaching



  • Fall 2021: EECS 498/598-007: Automated Formal Verification of Hardware and Software.

Links