Research Commons
      • Browse 
        • Communities & Collections
        • Titles
        • Authors
        • By Issue Date
        • Subjects
        • Types
        • Series
      • Help 
        • About
        • Collection Policy
        • OA Mandate Guidelines
        • Guidelines FAQ
        • Contact Us
      • My Account 
        • Sign In
        • Register
      View Item 
      •   Research Commons
      • University of Waikato Research
      • General
      • General Papers
      • View Item
      •   Research Commons
      • University of Waikato Research
      • General
      • General Papers
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.

      Shape predicates allow unbounded verification of linearizability using canonical abstraction

      Friggens, David; Groves, Lindsay
      Thumbnail
      Files
      CRPITV147Friggens.pdf
      417.7Kb
      Link
       crpit.com
      Citation
      Export citation
      Friggens, 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).
      Permanent Research Commons link: https://hdl.handle.net/10289/8572
      Abstract
      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.
      Date
      2014
      Type
      Conference Contribution
      Publisher
      Australian Computer Society Inc
      Rights
      Copyright © 2014, the authors. Reproduction for academic, not-for-profit purposes permitted provided this text is included.
      Collections
      • General Papers [47]
      Show full item record  

      Usage

      Downloads, last 12 months
      21
       
       

      Usage Statistics

      For this itemFor all of Research Commons

      The University of Waikato - Te Whare Wānanga o WaikatoFeedback and RequestsCopyright and Legal Statement