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

simulationconcurrencyI/O automatalinearisabilitylock-free algorithms

Mathematics Subject Classification ID

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)

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

(13)

• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Towards formally specifying and verifying transactional memory
• Proving linearizability with temporal logic
• Simulation Refinement for Concurrency Verification
• 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
• Testing and verifying concurrent objects
• A sound and complete proof technique for linearizability of concurrent data structures
• 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)