Verifying concurrent data structures by simulation

MaRDI QIDQ2863833zbMATH OpenFDO

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

zbMATH Keywords

concurrencyI/O automatalinearisabilitylock-free algorithmssimulation

Mathematics Subject Classification ID

Data structures (68P05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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

Cited in

(14)

• Testing and verifying concurrent objects
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• A sound and complete proof technique for linearizability of concurrent data structures
• Decomposable relaxation for concurrent data structures
• Reasoning about nonblocking concurrency
• Nonblocking Algorithms and Backward Simulation
• scientific article; zbMATH DE number 1487480 (Why is no real title available?)
• Towards formally specifying and verifying transactional memory
• Computer Aided Verification
• An integrated specification and verification technique for highly concurrent data structures
• Proving linearizability with temporal logic
• Simulation Refinement for Concurrency Verification
• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• A fine-grained semantics for arrays and pointers under weak memory models

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)