Show simple item record  

dc.contributor.authorFriggens, David
dc.contributor.authorGroves, Lindsay
dc.date.accessioned2014-03-24T03:47:36Z
dc.date.available2014-03-24T03:47:36Z
dc.date.issued2014
dc.identifier.citationFriggens, D. & Groves, L. (2014). Shape predicates allow unbounded verification of linearizability using canonical abstraction. In B. H. Thomas & D. Parry (Eds.), Proceedings of the Thirty-Seventh Australasian Computer Science Conference (ACSC 2014), CRPIT. 147. Auckland, New Zealand (pp. 49-56).en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/8572
dc.description.abstractCanonical abstraction is a static analysis technique that represents states as 3-valued logical structures, and is able to construct finite representations of systems with infinite statespaces for verification. The granularity of the abstraction can be altered by the definition of instrumentation predicates, which derive their meaning from other predicates. We introduce shape predicates for preserving certain structures of the state during abstraction. We show that shape predicates allow linearizability to be verified for concurrent data structures using canonical abstraction alone, and use the approach to verify a stack and two queue algorithms. This contrasts with previous efforts to verify linearizability with canonical abstraction, which have had to employ other techniques as well.en_NZ
dc.format.mimetypeapplication/pdf
dc.language.isoenen_NZ
dc.publisherAustralian Computer Society Incen_NZ
dc.relation.urihttp://crpit.com/abstracts/CRPITV147Friggens.htmlen_NZ
dc.rightsCopyright © 2014, the authors. Reproduction for academic, not-for-profit purposes permitted provided this text is included.en_NZ
dc.subjectcanonical abstractionen_NZ
dc.subjectconcurrent data structuresen_NZ
dc.subjectlinearizabilityen_NZ
dc.subjectverificationen_NZ
dc.subjectcomputer science
dc.subjectformal methods
dc.titleShape predicates allow unbounded verification of linearizability using canonical abstractionen_NZ
dc.typeConference Contributionen_NZ


Files in this item

This item appears in the following Collection(s)

Show simple item record