Yatin A. Manerkar

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