Conferences in Research and Practice in Information Technology
  

Online Version - Last Updated - 20 Jan 2012

 

 
Home
 

 
Procedures and Resources for Authors

 
Information and Resources for Volume Editors
 

 
Orders and Subscriptions
 

 
Published Articles

 
Upcoming Volumes
 

 
Contact Us
 

 
Useful External Links
 

 
CRPIT Site Search
 
    

Shape Predicates Allow Unbounded Veri cation of Linearizability Using Canonical Abstraction

Friggens, D. and Groves, L.

    Canonical 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.
Cite as: Friggens, D. and Groves, L. (2014). Shape Predicates Allow Unbounded Veri cation of Linearizability Using Canonical Abstraction. In Proc. Thirty-Seventh Australasian Computer Science Conference (ACSC 2014) Auckland, New Zealand. CRPIT, 147. Thomas, B. and Parry, D. Eds., ACS. 49-56
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS