This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Yatin A. Manerkar
A grouping.
Yatin A. Manerkar: formal memory-consistency verification across the stack - TriCheck, RealityCheck, UCLID5, SemPat's hyperproperty-based test generation, and takoFormal for programmable memory.
5 references
takoFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)
Pranav Srinivasan and others (2026)
SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns
Adwait Godbole and others (2024)
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen and others (2022) · Computer Aided Verification · Springer
RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification
Yatin A. Manerkar and others (2020)
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
Caroline Trippel and others (2017) · Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2017)