Yatin A. Manerkar

According to our database, Yatin A. Manerkar authored at least 19 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns.

Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia

CoRR, 2024

Lifting Micro-Update Models from RTL for Formal Security Analysis.

Adwait Godbole, Kevin Cheang, Yatin A. Manerkar, Sanjit A. Seshia

Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024

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., October, 2023

Kobold: Simplified Cache Coherence for Cache-Attached Accelerators.

Jennifer Brana, Brian C. Schwedock, Yatin A. Manerkar, Nathan Beckmann

IEEE Comput. Archit. Lett., 2023

Modelling and Verification of Security-Oriented Resource Partitioning Schemes.

Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, Sanjit A. Seshia

Proceedings of the Formal Methods in Computer-Aided Design, 2023

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency.

Chase Norman, Adwait Godbole, Yatin A. Manerkar

Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2023

2022

MOESI-prime: preventing coherence-induced hammering in commodity workloads.

Kevin Loughlin, Stefan Saroiu, Alec Wolman, Yatin A. Manerkar, Baris Kasikci

Proceedings of the ISCA '22: The 49th Annual International Symposium on Computer Architecture, New York, New York, USA, June 18, 2022

Automated Conversion of Axiomatic to Operational Models: Theory and Practice.

Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

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

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021

Progressive Automated Formal Verification of Memory Consistency in Parallel Processors

Yatin A. Manerkar

PhD thesis, 2021

2020

RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification.

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi

CoRR, 2020

2018

Full-Stack Memory Model Verification with TriCheck.

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi

IEEE Micro, 2018

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications.

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Aarti Gupta

Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture, 2018

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

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

RTLcheck: verifying the memory consistency of RTL designs.

Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, Michael Pellauer

Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture, 2017

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA.

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi

Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, 2017

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

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

2015

CCICheck: using µhb graphs to verify the coherence-consistency interface.

Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi

Proceedings of the 48th International Symposium on Microarchitecture, 2015