CCICheck: using µhb graphs to verify the coherence-consistency interface. - Yatin A. Manerkar; Daniel Lustig; Michael Pellauer; Margaret Martonosi (MICRO, 2015)

Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. - Yatin A. Manerkar; Caroline Trippel; Daniel Lustig; Michael Pellauer; Margaret Martonosi (CoRR, 2016)

Exploring the Trisection of Software, Hardware, and ISA in Memory Model Design. - Caroline Trippel; Yatin A. Manerkar; Daniel Lustig; Michael Pellauer; Margaret Martonosi (CoRR, 2016)

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. - Caroline Trippel; Yatin A. Manerkar; Daniel Lustig; Michael Pellauer; Margaret Martonosi (ASPLOS, 2017)

RTLcheck: verifying the memory consistency of RTL designs. - Yatin A. Manerkar; Daniel Lustig; Margaret Martonosi; Michael Pellauer (MICRO, 2017)

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 (FMCAD, 2018)

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. - Yatin A. Manerkar; Daniel Lustig; Margaret Martonosi; Aarti Gupta (MICRO, 2018)

Full-Stack Memory Model Verification with TriCheck. - Caroline Trippel; Yatin A. Manerkar; Daniel Lustig; Michael Pellauer; Margaret Martonosi (IEEE Micro, 2018)

RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification. - Yatin A. Manerkar; Daniel Lustig; Margaret Martonosi (CoRR, 2020)

Progressive Automated Formal Verification of Memory Consistency in Parallel Processors - Yatin A. Manerkar (2021)

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 002; Sanjit A. Seshia (CAV (1), 2022)

Automated Conversion of Axiomatic to Operational Models: Theory and Practice. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (FMCAD, 2022)

MOESI-prime: preventing coherence-induced hammering in commodity workloads. - Kevin Loughlin; Stefan Saroiu; Alec Wolman; Yatin A. Manerkar; Baris Kasikci (ISCA, 2022)

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. - Chase Norman; Adwait Godbole; Yatin A. Manerkar (ASPLOS (3), 2023)

Modelling and Verification of Security-Oriented Resource Partitioning Schemes. - Adwait Godbole; Leiqi Ye; Yatin A. Manerkar; Sanjit A. Seshia (FMCAD, 2023)

Kobold: Simplified Cache Coherence for Cache-Attached Accelerators. - Jennifer Brana; Brian C. Schwedock; Yatin A. Manerkar; Nathan Beckmann (IEEE Comput. Archit. Lett., 2023)

Towards Building Verifiable CPS using Lingua Franca. - Shaokai Lin; Yatin A. Manerkar; Marten Lohstroh; Elizabeth Polgreen; Sheng-Jung Yu; Chadlia Jerad; Edward A. Lee; Sanjit A. Seshia (ACM Trans. Embed. Comput. Syst., 2023)

Lifting Micro-Update Models from RTL for Formal Security Analysis. - Adwait Godbole; Kevin Cheang; Yatin A. Manerkar; Sanjit A. Seshia (ASPLOS (2), 2024)

SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (CCS, 2024)

SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (CoRR, 2024)