Yatin Manerkar

I am an incoming Royal Society Wolfson Visiting Fellow at the University of Edinburgh, and an Adjunct 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.

My research addresses the challenge of creating correct computing systems by developing automated formal methodologies and tools for the design, verification, and synthesis of computing systems. Verification using formal methods provides strong correctness guarantees based on mathematical proofs, while formal synthesis can generate models and implementations that are guaranteed to respect correctness properties. My work spans the hardware/software stack, from high-level programming languages down to low-level Verilog circuits.

More specifically, my research lies at the boundary between formal methods, computer architecture, and AI, with a focus on concurrency and hardware security. A key theme in my research is making formal methods easier for non-experts to use, enabling more people in industry and academia to leverage their power to create correct computing systems. I am also passionate about developing formalisms for emerging hardware (including AI hardware) and verifying that such hardware works correctly. 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). Some of my recent work has been used for verification at Intel. 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. I have also received three Distinguished Reviewer Awards from the PLDI and ASPLOS conferences. Additionally, 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).

Before studying at 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.

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, emerging architectures, and neurosymbolic approaches that combine AI and formal methods. Some of these projects have already generated publications.

Research Statement (a bit dated, but still relevant)

PhD Students

Pranav Srinivasan (co-advised with Manos Kapritsos)

Undergraduate Students

Current

Vadim Monakhov (2025 - Present)
Zohra Younus (2026 - Present)
Thomas Rogers (2026 - Present)
Xinhao Tong (2026 - Present)
Zachary Hoheb (2026 - Present)
Aravind Kandarpa (2026 - Present)

Notable Alumni

Rishabh Chandel (U Michigan '26, now a PhD student at Rutgers University)
Luke Miga (U Michigan '25, now a PhD student at Purdue University)
Yue Huang (U Michigan '24, subsequently MEng at UC Berkeley)
Leiqi Ye (U Michigan '23, now a PhD student at University of Edinburgh)
Jennifer Brana (U of Portland '23, subsequently a PhD student at Carnegie Mellon University) (co-mentored with Nathan Beckmann)
Chase Norman (UC Berkeley '23, now a PhD student at Carnegie Mellon University)

Publications

Refereed Publications

Pranav Srinivasan, Manos Kapritsos, and Yatin A. Manerkar. takoFormal: Enabling Robust Software for Programmable Memory Hierarchies. The 53rd IEEE/ACM International Symposium on Computer Architecture (ISCA), June 2026.
[PDF] [Extended Version] [Talk Video] [GitHub]
Adwait Godbole, Yatin A. Manerkar, and Sanjit A. Seshia. SemPat: Using Hyperproperty-based Semantic Analysis to Generate Attack Patterns. The ACM Conference on Computer and Communications Security (ACM CCS) 2024, October 2024.
[PDF]
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.
[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. ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions 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

Unlocking the AI Stack With Formal Methods.
NVIDIA Research, Westford, MA, April 2026.
Formal Methods for the Age of Accelerators.
Synopsys, Santa Clara, CA, February 2026.
Formal Methods for the AI Era: Challenges and Opportunities.
Google DeepMind, Mountain View, CA, October 2025.
Hair of the Dog: How AI Can Help Formally Verify AI-Designed Chips.
AI For Fully-Automated Chip Design Workshop at ISCA 2025, Tokyo, Japan, June 2025.
Using Formal Methods to Ensure Correctness for Hardware-Software Codesign.
Michigan Institute for Computational Discovery and Engineering (MICDE), University of Michigan, Ann Arbor, MI, October 2024.
Formal Methods for Computer Architecture: Reducing the Barriers to Entry
University of Pennsylvania, Philadelphia, PA, December 2023.
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. (joint talk with Elizabeth Polgreen)
Workshop on Democratizing Software Verification (DSV), Haifa, Israel, August 2022.
Why is Ethical AI hard? A Technical Perspective.
Ethics of AI Learning Cohort, Princeton University, Princeton NJ, November 2021.
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 2026: EECS 370: Intro to Computer Organization
Fall 2025: EECS 370: Intro to Computer Organization
Winter 2025: EECS 370: Intro to Computer Organization
Fall 2024: EECS 498/598: Automated Formal Verification
Winter 2024: EECS 370: Intro to Computer Organization (2 sections)
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: Automated Formal Verification of Hardware and Software.