10.1184/R1/6626468.v1 Hannes Mehnert Hannes Mehnert Jonathan Aldrich Jonathan Aldrich Verification of Snapshotable Trees using Access Permissions and Typestate Carnegie Mellon University 2012 Software Research 2012-05-01 00:00:00 Journal contribution https://kilthub.cmu.edu/articles/journal_contribution/Verification_of_Snapshotable_Trees_using_Access_Permissions_and_Typestate/6626468 <p>We use access permissions and typestate to specify and verify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe the challenges to verifying snapshotable trees in Plural, give an abstract interface specification against which we verify the client code, provide a concrete specification for an implementation and describe proof patterns we found. We also relate this verification approach to other techniques used to verify this data structure.</p>