| 2026 | ISCA | TKōFormal: Enabling Robust Software for Programmable Memory Hierarchies. | Pranav Srinivasan, Manos Kapritsos, Yatin A. Manerkar |
| 2024 | ASPLOS | Lifting Micro-Update Models from RTL for Formal Security Analysis. | Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, Sanjit A. Seshia |
| 2024 | CCS | SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security. | Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia |
| 2023 | ASPLOS | PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. | Chase Norman, Adwait Godbole, Yatin A. Manerkar |
| 2023 | FMCAD | Modelling and Verification of Security-Oriented Resource Partitioning Schemes. | Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, Sanjit A. Seshia |
| 2022 | CAV | UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. | Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia |
| 2022 | FMCAD | Automated Conversion of Axiomatic to Operational Models: Theory and Practice. | Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia |
| 2022 | ISCA | MOESI-prime: preventing coherence-induced hammering in commodity workloads. | Kevin Loughlin, Stefan Saroiu, Alec Wolman, Yatin A. Manerkar, Baris Kasikci |
| 2018 | FMCAD | ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. | Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik |
| 2018 | MICRO | PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. | Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta |
| 2017 | ASPLOS | TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. | Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi |
| 2017 | MICRO | RTLcheck: verifying the memory consistency of RTL designs. | Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer |
| 2015 | MICRO | CCICheck: using hb graphs to verify the coherence-consistency interface. | Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi |