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>