Formal verification of a concurrent binary search tree

Simple item page
dc.contributor.advisorRuppert, Eric
dc.contributor.advisorvan Breugel, Franck
dc.creatorChen, Xiwen
dc.date.accessioned2016-08-03T16:51:42Z
dc.date.available2016-08-03T16:51:42Z
dc.date.copyright2013-08
dc.degree.disciplineComputer Science and Engineering
dc.degree.levelMaster's
dc.degree.nameMSc - Master of Science
dc.description.abstractIn this thesis, we formally verify a simplified version of the non-blocking linearizable binary search tree of Ellen et al., which appeared in the Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing (pages 131-140), using the PVS specification and verification system. The algorithm and its specification are both modelled as I/O automata. In order to formally verify that the algorithm implements the specification, we show that the algorithm's I/O automaton simulates the specification's. An intermediate I/O automaton is constructed to simplify the simulation proof of linearizability. By showing there is a forward simulation from the algorithm's I/O automaton to the intermediate automaton and there is a backward simulation from the intermediate automaton to the specification's automaton, we formally verify that the algorithm implements its specification. While formalizing the proof, we found small errors in the original proof.
dc.identifier.urihttp://hdl.handle.net/10315/31700
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subject.keywordsconcurrent binary search tree
dc.subject.keywordsI/O automation
dc.subject.keywordsPVS specification
dc.titleFormal verification of a concurrent binary search tree
dc.typeElectronic Thesis or Dissertation

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Chen_Xiwen_2013_Masters.pdf
Size:
3.87 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.83 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
YorkU_ETDlicense.txt
Size:
3.37 KB
Format:
Plain Text
Description:
Download

Collections

Computer Science and Engineering

All items in the YorkSpace institutional repository are protected by copyright, with all rights reserved except where explicitly noted.