Verifying Linearizability of Intel® Software Guard Extensions
Abstract elided by the publisher.
Related papers
- Who guards the guards? formal validation of the Arm v8-m architecture specification OOPSLA 2017
- A Fully Verified Persistency Library VMCAI 2024
- Shape-Value Abstraction for Verifying Linearizability VMCAI 2009
- Comparison Under Abstraction for Verifying Linearizability CAV 2007
- A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability POPL 2024
- Mechanically verified proof obligations for linearizability TOPLAS 2011
- Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86 OOPSLA 2020
- C4: verified transactional objects OOPSLA 2022