Certified Reasoning in Memory Hierarchies
Abstract elided by the publisher.
Related papers
- FreeSpec: specifying, verifying, and executing impure computations in Coq CPP 2020
- A refinement hierarchy for free list memory allocators ISMM 2017
- Sequential reasoning for optimizing compilers under weak memory concurrency PLDI 2022
- Certified self-modifying code PLDI 2007
- Data-centric Multi-level Blocking PLDI 1997
- A comparison of programming models for multiprocessors with explicitly managed memory hierarchies PPoPP 2009
- A type system for certified binaries TOPLAS 2005
- A Hierarchy of Supermartingales for ω-Regular Verification PLDI 2026