Verifying Concurrent Data Structures by Simulation Export

@article{citeulike:565335, abstract = {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.}, author = {Colvin, Robert and Doherty, Simon and Groves, Lindsay}, booktitle = {Proceedings of the REFINE 2005 Workshop (REFINE 2005)}, citeulike-article-id = {565335}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.entcs.2005.04.026}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B75H1-4GM9P1Y-6/2/3bfecd5c391728e09e46d20589f08d11}, day = {21}, doi = {10.1016/j.entcs.2005.04.026}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {concurrency, io\_automata, linearisability, lock-free, simulation}, month = {July}, number = {2}, pages = {93--110}, posted-at = {2006-03-27 11:55:31}, priority = {0}, title = {Verifying Concurrent Data Structures by Simulation}, url = {http://dx.doi.org/10.1016/j.entcs.2005.04.026}, volume = {137}, year = {2005} }

TY - JOUR ID - citeulike:565335 L3 - citeulike-article-id:565335 N2 - 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. IS - 2 JF - Electronic Notes in Theoretical Computer Science EP - 110 TI - Verifying Concurrent Data Structures by Simulation VL - 137 T2 - Proceedings of the REFINE 2005 Workshop (REFINE 2005) SP - 93 KW - concurrency KW - io_automata KW - linearisability KW - lock-free KW - simulation AU - Colvin, Robert AU - Doherty, Simon AU - Groves, Lindsay PY - 2005/07/21/ UR - http://dx.doi.org/10.1016/j.entcs.2005.04.026 ER -