Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware

Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, Ronghui Gu
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles
SOSP '21
Virtual Event, Germany
Association for Computing Machinery
New York, NY, USA
Pages 866-881
Note(s): weak memory, Arm architecture, Operating systems, hypervisor, ISA specification