Formal verification of an array-based nonblocking queue

Colvin, Robert and Groves, Lindsay (2005). Formal verification of an array-based nonblocking queue. In: IEEE: Proceedings of the 10th IEEE International Conference. ICECCS 2005: Engineering of Complex Computer Systems, Shanghai, China, (507-516). 16-20 June 2005. doi:10.1109/ICECCS.2005.49

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

Author Colvin, Robert
Groves, Lindsay
Title of paper Formal verification of an array-based nonblocking queue
Conference name ICECCS 2005: Engineering of Complex Computer Systems
Conference location Shanghai, China
Conference dates 16-20 June 2005
Proceedings title IEEE: Proceedings of the 10th IEEE International Conference
Journal name Iceccs 2005: 10th Ieee International Conference On Engineering of Complex Computer Systems, Proceedings
Place of Publication Piscataway, NJ, United States
Publisher IEEE
Publication Year 2005
Sub-type Fully published paper
DOI 10.1109/ICECCS.2005.49
ISBN 076952284X
Start page 507
End page 516
Total pages 10
Language eng
Abstract/Summary We describe an array-based nonblocking implementation of a concurrent bounded queue, due to Shann, Huang and Chen (2000), and explain how we detected errors in the algorithm while attempting a formal verification. We explain how we first corrected the errors, and then modified the algorithm to obtain nonblocking behaviour in the boundary cases. Both the corrected and modified versions of the algorithm were verified using the PVS theorem proven. We describe the verification of the modified algorithm, which subsumes the proof of the corrected version.
Subjects 08 Information and Computing Sciences
0803 Computer Software
080309 Software Engineering
Keyword Computer engineering
Systems design
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status Non-UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 8 times in Thomson Reuters Web of Science Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 11 Apr 2006, 00:40:18 EST