| TriCheck: Memory model verification at the trisection of software, hardware, and ISA C Trippel, YA Manerkar, D Lustig, M Pellauer, M Martonosi ACM SIGPLAN Notices 52 (4), 119-133, 2017 | 79 | 2017 |
| CCICheck: Using µhb graphs to verify the coherence-consistency interface YA Manerkar, D Lustig, M Pellauer, M Martonosi Proceedings of the 48th International Symposium on Microarchitecture, 26-37, 2015 | 58 | 2015 |
| RTLCheck: Verifying the memory consistency of RTL designs YA Manerkar, D Lustig, M Martonosi, M Pellauer Proceedings of the 50th Annual IEEE/ACM International Symposium on …, 2017 | 49 | 2017 |
| Moesi-prime: preventing coherence-induced hammering in commodity workloads K Loughlin, S Saroiu, A Wolman, YA Manerkar, B Kasikci Proceedings of the 49th Annual International Symposium on Computer …, 2022 | 40 | 2022 |
| Counterexamples and proof loophole for the C/C++ to POWER and ARMv7 trailing-sync compiler mappings YA Manerkar, C Trippel, D Lustig, M Pellauer, M Martonosi arXiv preprint arXiv:1611.01507, 2016 | 32 | 2016 |
| ILA-MCM: integrating memory consistency models with instruction-level abstractions for heterogeneous system-on-chip verification H Zhang, C Trippel, YA Manerkar, A Gupta, M Martonosi, S Malik 2018 Formal Methods in Computer Aided Design (FMCAD), 1-10, 2018 | 23* | 2018 |
| PipeProof: Automated memory consistency proofs for microarchitectural specifications YA Manerkar, D Lustig, M Martonosi, A Gupta 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture …, 2018 | 22 | 2018 |
| UCLID5: multi-modal formal modeling, verification, and synthesis E Polgreen, K Cheang, P Gaddamadugu, A Godbole, K Laeufer, S Lin, ... International Conference on Computer Aided Verification, 538-551, 2022 | 17 | 2022 |
| Towards building verifiable CPS using Lingua Franca S Lin, YA Manerkar, M Lohstroh, E Polgreen, SJ Yu, C Jerad, EA Lee, ... ACM Transactions on Embedded Computing Systems 22 (5s), 1-24, 2023 | 9 | 2023 |
| Full-stack memory model verification with tricheck C Trippel, YA Manerkar, D Lustig, M Pellauer, M Martonosi IEEE Micro 38 (3), 58-68, 2018 | 6 | 2018 |
| Kobold: Simplified cache coherence for cache-attached accelerators J Brana, BC Schwedock, YA Manerkar, N Beckmann IEEE Computer Architecture Letters 22 (1), 41-44, 2023 | 5 | 2023 |
| Automated Conversion of Axiomatic to Operational Models: Theory and Practice. A Godbole, YA Manerkar, SA Seshia FMCAD, 331-342, 2022 | 4 | 2022 |
| RealityCheck: Bringing modularity, hierarchy, and abstraction to automated microarchitectural memory consistency verification YA Manerkar, D Lustig, M Martonosi arXiv preprint arXiv:2003.04892, 2020 | 4 | 2020 |
| Lifting Micro-Update Models from RTL for Formal Security Analysis A Godbole, K Cheang, YA Manerkar, SA Seshia Proceedings of the 29th ACM International Conference on Architectural …, 2024 | 2 | 2024 |
| Progressive Automated Formal Verification of Memory Consistency in Parallel Processors YA Manerkar Princeton University, 2021 | 2 | 2021 |
| SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns A Godbole, YA Manerkar, SA Seshia arXiv preprint arXiv:2406.05403, 2024 | 1 | 2024 |
| Modelling and Verification of Security-Oriented Resource Partitioning Schemes. A Godbole, L Ye, YA Manerkar, SA Seshia FMCAD, 268-273, 2023 | 1 | 2023 |
| Compositional Proofs of Information Flow Properties for Hardware-Software Platforms K Cheang, A Godbole, YA Manerkar, SA Seshia Tech. rep. UCB/EECS-2023-204. EECS Department, University of California …, 2023 | 1 | 2023 |
| PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency C Norman, A Godbole, YA Manerkar Proceedings of the 28th ACM International Conference on Architectural …, 2023 | 1 | 2023 |
| SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security A Godbole, YA Manerkar, SA Seshia Proceedings of the 2024 on ACM SIGSAC Conference on Computer and …, 2024 | | 2024 |
