Verifying concurrent data structures by simulation

Colvin, Robert, Doherty, Simon and Groves, Lindsay (2005). Verifying concurrent data structures by simulation. In: Proceedings of the REFINE 2005 Workshop. REFINE 2005 Workshop, Guildford, England, UK, (93-110). April, 2005. doi:10.1016/j.entcs.2005.04.026

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Colvin, Robert
Doherty, Simon
Groves, Lindsay
Title of paper Verifying concurrent data structures by simulation
Conference name REFINE 2005 Workshop
Conference location Guildford, England, UK
Conference dates April, 2005
Proceedings title Proceedings of the REFINE 2005 Workshop   Check publisher's open access policy
Journal name Electronic Notes in Theoretical Computer Science   Check publisher's open access policy
Place of Publication Amsterdam, Netherlands
Publisher Elsevier
Publication Year 2005
Year available 2005
Sub-type Fully published paper
DOI 10.1016/j.entcs.2005.04.026
ISSN 1571-0661
Volume 137
Issue 2
Start page 93
End page 110
Total pages 18
Language eng
Abstract/Summary We describe an approach to verifying concurrent data structures based on simulation between two Input/Output Automata (IOAs), modelling the specification and the implementation. We explain how we used this approach in mechanically verifying a simple lock-free stack implementation using forward simulation, and briefly discuss our experience in verifying three other lock-free algorithms which all required the use of backward simulation
Subjects 080309 Software Engineering
Keyword Concurrency
Lock-free algorithms
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Non-UQ

Version Filter Type
Citation counts: Scopus Citation Count Cited 24 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 12 Jan 2009, 09:42:58 EST by Ms Lynette Adams on behalf of Library Corporate Services