Verifying correctness of persistent concurrent data structures: a sound and complete method
From MaRDI portal
Publication:1982636
DOI10.1007/S00165-021-00541-8OpenAlexW3162279086MaRDI QIDQ1982636
Gerhard Schellhorn, John Derrick, Heike Wehrheim, Simon Doherty, Brijesh Dongol
Publication date: 14 September 2021
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-021-00541-8
Related Items (4)
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Unnamed Item ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system
Cites Work
- Unnamed Item
- Unnamed Item
- Forward and backward simulations. I. Untimed Systems
- A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
- Proving Opacity of a Pessimistic {STM}
- Tentative steps toward a development method for interfering programs
- Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
- A Unified Memory Model for Pointers
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
This page was built for publication: Verifying correctness of persistent concurrent data structures: a sound and complete method
