Profile picture

I am an Assistant Professor in the Computer Science and Engineering (CSE) Division at the University of Michigan. I 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 for part of 2021.

I am recruiting 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/systems and formal methods, and focuses on developing automated formal methodologies and tools for the design, verification, and synthesis of computing systems. My work spans the hardware/software stack, from high-level programming languages down to low-level Verilog circuits. Specific areas that interest me include the formal modelling, verification, and synthesis of emerging heterogeneous parallel hardware, hardware security, memory consistency models (MCMs), cache coherence, and ethical AI.

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. Three of my papers have been nominated or selected for best paper awards, and three of my papers have been selected as IEEE Micro Top Picks or Honorable Mentions for their high potential impact. My dissertation also received an ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award Honorable Mention for 2021.

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

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. Current verification processes have proven inadequate for catching these bugs, resulting in the release of flawed hardware and software.

My work focuses on addressing the challenge of creating correct computing systems through formal methods, including modelling, verification, and synthesis. Formal modelling involves developing formalisms for computing systems that are capable of capturing their behaviour effectively and efficiently. Verification using formal methods, meanwhile, provides strong correctness guarantees based on mathematical proofs, and is adept at catching hard-to-find bugs. Finally, formal synthesis can automatically generate correct models or implementations of systems from high-level correctness specifications. Specific subject areas in systems that my formal methods research is currently investigating include memory consistency, security, cache coherence, and emerging architectures. Some of these projects have already generated publications.

Research Statement (a bit dated, but still relevant)

PhD Students



  • Yan-Ru Jhou
  • Pranav Srinivasan (co-advised with Manos Kapritsos)

Publications



Refereed Publications

  • Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, and Sanjit A. Seshia. Lifting Micro-Update Models from RTL for Formal Security Analysis. The 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2024.
    [PDF]

  • Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, and Sanjit A. Seshia. Modelling and Verification of Security-Oriented Resource Partitioning Schemes. The 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2023.
    [PDF]

  • Shaokai Lin, Yatin A. Manerkar, Marten Lohstroh, Elizabeth Polgreen, Sheng-Jung Yu, Chadlia Jerad, Edward A. Lee, and Sanjit A. Seshia. Towards Building Verifiable CPS using Lingua Franca. The International Conference on Embedded Software (EMSOFT) 2023, September 2023.
    [PDF]

  • Jennifer Brana, Brian C. Schwedock, Yatin A. Manerkar, and Nathan Beckmann. Kobold: Simplified Cache Coherence For Cache-Attached Accelerators. IEEE Computer Architecture Letters, April 2023.
    [PDF]

  • Chase Norman, Adwait Godbole, and Yatin A. Manerkar. PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. The 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2023.
    [PDF]

  • Adwait Godbole, Yatin A. Manerkar, and Sanjit A. Seshia. Automated Conversion of Axiomatic to Operational Models: Theory and Practice. The 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2022.
    Selected as one of the best papers of FMCAD 2022.
    Invited to submit an extended version to an FMSD (Formal Methods in System Design) special issue.

    [PDF]

  • Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. Seshia. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. The 34th International Conference on Computer Aided Verification (CAV), August 2022.
    [PDF]

  • Kevin Loughlin, Stefan Saroiu, Alec Wolman, Yatin A. Manerkar, and Baris Kasikci. MOESI-prime: Preventing Coherence-Induced Hammering in Commodity Workloads. The 49th International Symposium on Computer Architecture (ISCA), June 2022.
    [PDF]

  • 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.
    Received an ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award Honorable Mention for 2021.
    [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



  • Winter 2023: EECS 570: Parallel Computer Architecture. (Enrollment Policy)

  • Fall 2022: EECS 370: Intro to Computer Organization and Design.

  • Winter 2022: EECS 570: Parallel Computer Architecture.

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

Links