Yatin A. Manerkar

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 19

Top Topics

Computing Power

Automated Theorem Provers

Semantic Analysis

Top Venues

Publications

Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, Sanjit A. Seshia
Lifting Micro-Update Models from RTL for Formal Security Analysis. ASPLOS (2) (2024)
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns. CoRR (2024)
Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, Sanjit A. Seshia
Modelling and Verification of Security-Oriented Resource Partitioning Schemes. FMCAD (2023)
Shaokai Lin, Yatin A. Manerkar, Marten Lohstroh, Elizabeth Polgreen, Sheng-Jung Yu, Chadlia Jerad, Edward A. Lee, Sanjit A. Seshia
Towards Building Verifiable CPS using Lingua Franca. ACM Trans. Embed. Comput. Syst. 22 (5s) (2023)
Chase Norman, Adwait Godbole, Yatin A. Manerkar
PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. ASPLOS (3) (2023)
Jennifer Brana, Brian C. Schwedock, Yatin A. Manerkar, Nathan Beckmann
Kobold: Simplified Cache Coherence for Cache-Attached Accelerators. IEEE Comput. Archit. Lett. 22 (1) (2023)
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. CoRR (2022)
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
Automated Conversion of Axiomatic to Operational Models: Theory and Practice. FMCAD (2022)
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
Automated Conversion of Axiomatic to Operational Models: Theory and Practice. CoRR (2022)
Kevin Loughlin, Stefan Saroiu, Alec Wolman, Yatin A. Manerkar, Baris Kasikci
MOESI-prime: preventing coherence-induced hammering in commodity workloads. ISCA (2022)
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, Sanjit A. Seshia
UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. CAV (1) (2022)
Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi
RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification. CoRR (2020)
Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi
Full-Stack Memory Model Verification with TriCheck. IEEE Micro 38 (3) (2018)
Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta
PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications. MICRO (2018)
Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik
ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. FMCAD (2018)
Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer
RTLcheck: verifying the memory consistency of RTL designs. MICRO (2017)
Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. ASPLOS (2017)
Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, Margaret Martonosi
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR (2016)
Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi
Exploring the Trisection of Software, Hardware, and ISA in Memory Model Design. CoRR (2016)
Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi
CCICheck: using µhb graphs to verify the coherence-consistency interface. MICRO (2015)