Bodenmüller et al., 2023
ViewPDF| Publication | Publication Date | Title |
|---|---|---|
| Liang et al. | Modular verification of linearizability with non-fixed linearization points | |
| Feldman et al. | A wait-free multi-word compare-and-swap operation | |
| US8214833B2 (en) | Systems and methods for supporting software transactional memory using inconsistency-aware compilers and libraries | |
| Bodenmüller et al. | A fully verified persistency library | |
| Derrick et al. | Verifying correctness of persistent concurrent data structures: a sound and complete method | |
| Derrick et al. | Verifying correctness of persistent concurrent data structures | |
| Ridge | A rely-guarantee proof system for x86-TSO | |
| Bila et al. | Defining and verifying durable opacity: Correctness for persistent software transactional memory | |
| Khyzha et al. | Abstraction for crash-resilient objects | |
| Raad et al. | Intel PMDK transactions: specification, validation and concurrency | |
| Bila et al. | Modularising verification of durable opacity | |
| US8769514B2 (en) | Detecting race conditions with a software transactional memory system | |
| Dickerson et al. | Conflict abstractions and shadow speculation for optimistic transactional objects | |
| Holík et al. | Effect Summaries for Thread-Modular Analysis: Sound Analysis Despite an Unsound Heuristic | |
| Smith et al. | Admit your weakness: Verifying correctness on TSO architectures | |
| Schellhorn et al. | Adding concurrency to a sequential refinement tower | |
| US8490115B2 (en) | Ambient state for asynchronous methods | |
| Mutluergil et al. | A mechanized refinement proof of the Chase–Lev deque using a proof system | |
| He et al. | GPS+: Reasoning about fences and relaxed atomics | |
| Štill et al. | Weak memory models as LLVM-to-LLVM transformations | |
| Jonsson | Using refinement calculus techniques to prove linearizability | |
| Hassan et al. | Optimistic transactional boosting | |
| Dongol et al. | Checking opacity and durable opacity with FDR | |
| Štill et al. | Model checking of C++ programs under the x86-tso memory model | |
| Winter et al. | Observational models for linearizability checking on weak memory models |