Verifying concurrent data structures by simulation
From MaRDI portal
Publication:2863833
zbMATH Open1276.68062MaRDI QIDQ2863833FDOQ2863833
Authors: Robert Colvin, Simon Doherty, Lindsay Groves 
Publication date: 4 December 2013
Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066105050929?np=y
Recommendations
- Testing and verifying concurrent objects
- A sound and complete proof technique for linearizability of concurrent data structures
- An integrated specification and verification technique for highly concurrent data structures
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- Automatically verifying concurrent queue algorithms
Formal languages and automata (68Q45) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cited In (13)
- Verifying correctness of persistent concurrent data structures: a sound and complete method
- Towards formally specifying and verifying transactional memory
- Simulation Refinement for Concurrency Verification
- Proving linearizability with temporal logic
- Nonblocking Algorithms and Backward Simulation
- Decomposable relaxation for concurrent data structures
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
- Reasoning about nonblocking concurrency
- An integrated specification and verification technique for highly concurrent data structures
- A sound and complete proof technique for linearizability of concurrent data structures
- Testing and verifying concurrent objects
- A fine-grained semantics for arrays and pointers under weak memory models
- Computer Aided Verification
This page was built for publication: Verifying concurrent data structures by simulation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2863833)
