| 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 | 70 | 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 | 54 | 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 | 44 | 2017 |
| 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 | 29 | 2016 |
| 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 | 26 | 2022 |
| 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 | 19 | 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 | 19 | 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 | 10 | 2022 |
| Full-stack memory model verification with tricheck C Trippel, YA Manerkar, D Lustig, M Pellauer, M Martonosi IEEE Micro 38 (3), 58-68, 2018 | 5 | 2018 |
| 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 |
| Kobold: Simplified cache coherence for cache-attached accelerators J Brana, BC Schwedock, YA Manerkar, N Beckmann IEEE Computer Architecture Letters, 2023 | 2 | 2023 |
| Progressive Automated Formal Verification of Memory Consistency in Parallel Processors YA Manerkar Princeton University, 2021 | 2 | 2021 |
| 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 | 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 |
| 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 | | 2024 |
| Modelling and Verification of Security-Oriented Resource Partitioning Schemes A Godbole, L Ye, YA Manerkar, SA Seshia CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN–FMCAD 2023, 268, 2023 | | 2023 |
| Specifying and Generating Abstract Models for Formal Security Analysis A Godbole, K Cheang, Y Manerkar, SA Seshia | | 2023 |
| UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis A Godbole, K Laeufer, S Lin, YA Manerkar, F Mora, SA Seshia | | |
