Automatically verifying concurrent queue algorithms

MaRDI QIDQ2845500zbMATH OpenFDO

Authors Eran Yahav, Mooly Sagiv

Publication date 30 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105800064

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Parallel algorithms in computer science (68W10)

Recommendations

• Formal Techniques for Networked and Distributed Systems – FORTE 2004
• An integrated specification and verification technique for highly concurrent data structures
• Testing and verifying concurrent objects
• Checking linearizability of concurrent priority queues
• Safety and Liveness in Concurrent Pointer Programs

Cited in

(7)

• Analysing lock-free linearizable datatypes using CSP
• Verifying concurrent data structures by simulation
• Verifying concurrent graph algorithms
• scientific article; zbMATH DE number 1948389 (Why is no real title available?)
• scientific article; zbMATH DE number 1500569 (Why is no real title available?)
• An integrated specification and verification technique for highly concurrent data structures
• Formal Techniques for Networked and Distributed Systems – FORTE 2004

This page was built for publication: Automatically verifying concurrent queue algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2845500)